:: BAGORDER semantic presentation
theorem E1: :: BAGORDER:1
for b
1, b
2, b
3 being
set holds
( ( b
3 in b
1 & b
3 in b
2 ) implies ( ( b
1 \ {b3} = b
2 \ {b3} iff b
1 = b
2 ) ) )
proof
let c
1, c
2, c
3 be
set ;
assume E2:
( c
3 in c
1 & c
3 in c
2 )
;
thus
( c
1 = c
2 implies c
1 \ {c3} = c
2 \ {c3} )
;
end;
theorem :: BAGORDER:2
for b
1, b
2 being
Nat holds
( b
2 in Seg b
1 iff ( b
2 - 1 is
Nat & b
2 - 1
< b
1 ) )
theorem E2: :: BAGORDER:3
theorem E3: :: BAGORDER:4
proof
let c
1, c
2, c
3 be
Function;
assume that E4:
dom c
1 = dom c
2
and E5:
rng c
1 c= dom c
3
and E6:
rng c
2 c= dom c
3
and E7:
c
1,c
2 are_fiberwise_equipotent
;
consider c
4 being
Permutation of
dom c
1 such that E8:
c
1 = c
2 * c
4
by E4, E7, RFINSEQ:6;
E9:
dom (c3 * c1) = dom c
1
by E5, RELAT_1:46;
E10:
dom (c3 * c2) = dom c
2
by E6, RELAT_1:46;
c
3 * c
1 = (c3 * c2) * c
4
by E8, RELAT_1:55;
hence
c
3 * c
1,c
3 * c
2 are_fiberwise_equipotent
by E4, E9, E10, RFINSEQ:6;
end;
theorem E4: :: BAGORDER:5
definition
let c
1, c
2, c
3 be
Nat;
let c
4 be
ManySortedSet of c
1;
func c
2,c
3 -cut c
4 -> ManySortedSet of a
3 -' a
2 means :
E5:
:: BAGORDER:def 1
for b
1 being
Nat holds
( b
1 in a
3 -' a
2 implies a
5 . b
1 = a
4 . (a2 + b1) );
existence
ex b1 being ManySortedSet of c3 -' c2 st
for b2 being Nat holds
( b2 in c3 -' c2 implies b1 . b2 = c4 . (c2 + b2) )
proof
defpred S
1[
set ,
set ] means ex b
1 being
Nat st
( b
1 = a
1 & a
2 = c
4 . (c2 + b1) );
E5:
for b
1, b
2, b
3 being
set holds
( ( b
1 in c
3 -' c
2 & S
1[b
1,b
2] & S
1[b
1,b
3] ) implies ( b
2 = b
3 ) )
;
now
let c
5 be
set ;
assume E6:
c
5 in c
3 -' c
2
;
c
3 -' c
2 = { b1 where B is Nat : b1 < c3 -' c2 }
by AXIOMS:30;
then consider c
6 being
Nat such that E7:
( c
5 = c
6 & c
6 < c
3 -' c
2 )
by E6;
reconsider c
7 = c
5 as
Nat by E7;
consider c
8 being
set such that E8:
c
8 = c
4 . (c2 + c7)
;
take c
9 = c
8;
thus
S
1[c
5,c
9]
by E8;
end;
then E6:
for b
1 being
set holds
not ( b
1 in c
3 -' c
2 & ( for b
2 being
set holds
not S
1[b
1,b
2] ) )
;
consider c
5 being
Function such that E7:
dom c
5 = c
3 -' c
2
and E8:
for b
1 being
set holds
( b
1 in c
3 -' c
2 implies S
1[b
1,c
5 . b
1] )
from FUNCT_1:sch 2(E5, E6);
reconsider c
6 = c
5 as
ManySortedSet of c
3 -' c
2 by E7, PBOOLE:def 3;
take
c
6
;
let c
7 be
Nat;
assume E9:
c
7 in c
3 -' c
2
;
consider c
8 being
Nat such that E10:
( c
8 = c
7 & c
6 . c
7 = c
4 . (c2 + c8) )
by E8, E9;
thus
c
6 . c
7 = c
4 . (c2 + c7)
by E10;
end;
uniqueness
for b1, b2 being ManySortedSet of c3 -' c2 holds
( ( ( for b3 being Nat holds
( b3 in c3 -' c2 implies b1 . b3 = c4 . (c2 + b3) ) ) & ( for b3 being Nat holds
( b3 in c3 -' c2 implies b2 . b3 = c4 . (c2 + b3) ) ) ) implies ( b1 = b2 ) )
proof
let c
5, c
6 be
ManySortedSet of c
3 -' c
2;
assume that E5:
for b
1 being
Nat holds
( b
1 in c
3 -' c
2 implies c
5 . b
1 = c
4 . (c2 + b1) )
and E6:
for b
1 being
Nat holds
( b
1 in c
3 -' c
2 implies c
6 . b
1 = c
4 . (c2 + b1) )
;
E7:
( c
3 -' c
2 = dom c
5 & c
3 -' c
2 = dom c
6 )
by PBOOLE:def 3;
now
let c
7 be
set ;
assume E8:
c
7 in c
3 -' c
2
;
c
3 -' c
2 = { b1 where B is Nat : b1 < c3 -' c2 }
by AXIOMS:30;
then consider c
8 being
Nat such that E9:
( c
7 = c
8 & c
8 < c
3 -' c
2 )
by E8;
reconsider c
9 = c
7 as
Nat by E9;
c
5 . c
7 = c
4 . (c2 + c9)
by E5, E8;
hence
c
5 . c
7 = c
6 . c
7
by E6, E8;
end;
hence
c
5 = c
6
by E7, FUNCT_1:9;
end;
end;
:: deftheorem E5 defines -cut BAGORDER:def 1 :
theorem E6: :: BAGORDER:6
proof
let c
1, c
2 be
Nat;
let c
3, c
4 be
ManySortedSet of c
1;
set c
5 = 0,
(c2 + 1) -cut c
3;
set c
6 =
(c2 + 1),c
1 -cut c
3;
set c
7 = 0,
(c2 + 1) -cut c
4;
set c
8 =
(c2 + 1),c
1 -cut c
4;
thus
( c
3 = c
4 implies ( 0,
(c2 + 1) -cut c
3 = 0,
(c2 + 1) -cut c
4 &
(c2 + 1),c
1 -cut c
3 = (c2 + 1),c
1 -cut c
4 ) )
;
assume E7:
( 0,
(c2 + 1) -cut c
3 = 0,
(c2 + 1) -cut c
4 &
(c2 + 1),c
1 -cut c
3 = (c2 + 1),c
1 -cut c
4 )
;
E8:
now
let c
9 be
Nat;
assume E9:
c
9 in c
2 + 1
;
(c2 + 1) -' 0
= ((c2 + 1) + 0) -' 0
;
then E10:
c
9 in (c2 + 1) -' 0
by E9, BINARITH:39;
then
(0,(c2 + 1) -cut c4) . c
9 = c
4 . (0 + c9)
by E5;
hence
c
3 . c
9 = c
4 . c
9
by E7, E10, E5;
end;
E9:
now
let c
9 be
Nat;
assume E10:
( c
9 >= c
2 + 1 & c
9 < c
1 )
;
set c
10 = c
9 -' (c2 + 1);
E11:
c
9 - (c2 + 1) >= (c2 + 1) - (c2 + 1)
by E10, XREAL_1:11;
then E12:
c
9 -' (c2 + 1) = c
9 - (c2 + 1)
by BINARITH:def 3;
c
1 >= c
2 + 1
by E10, XXREAL_0:2;
then
c
1 - (c2 + 1) >= (c2 + 1) - (c2 + 1)
by XREAL_1:11;
then E13:
c
1 -' (c2 + 1) = c
1 - (c2 + 1)
by BINARITH:def 3;
c
9 - (c2 + 1) < c
1 - (c2 + 1)
by E10, REAL_1:92;
then E14:
c
9 -' (c2 + 1) in c
1 -' (c2 + 1)
by E12, E13, EULER_1:1;
then E15:
((c2 + 1),c1 -cut c3) . (c9 -' (c2 + 1)) = c
3 . ((c9 - (c2 + 1)) + (c2 + 1))
by E12, E5;
((c2 + 1),c1 -cut c4) . (c9 -' (c2 + 1)) = c
4 . ((c2 + 1) + (c9 -' (c2 + 1)))
by E14, E5;
hence
c
3 . c
9 = c
4 . c
9
by E7, E11, E15, BINARITH:def 3;
end;
now
let c
9 be
set ;
assume E10:
c
9 in c
1
;
c
1 = { b1 where B is Nat : b1 < c1 }
by AXIOMS:30;
then consider c
10 being
Nat such that E11:
( c
10 = c
9 & c
10 < c
1 )
by E10;
reconsider c
11 = c
9 as
Nat by E11;
per cases
not ( not c
11 in c
2 + 1 & c
11 in c
2 + 1 )
;
suppose
c
11 in c
2 + 1
;
hence
c
3 . c
9 = c
4 . c
9
by E8;
end;
suppose
not c
11 in c
2 + 1
;
then
( c
11 >= c
2 + 1 & c
11 < c
1 )
by E11, EULER_1:1;
hence
c
3 . c
9 = c
4 . c
9
by E9;
end;
end;
end;
hence
c
3 = c
4
by PBOOLE:3;
end;
:: deftheorem defines Fin BAGORDER:def 2 :
theorem E7: :: BAGORDER:7
proof
let c
1 be non
empty transitive antisymmetric RelStr ;
let c
2 be
finite Subset of c
1;
set c
3 = the
InternalRel of c
1;
set c
4 = the
carrier of c
1;
E8:
the
InternalRel of c
1 is_transitive_in the
carrier of c
1
by ORDERS_2:def 5;
E9:
the
InternalRel of c
1 is_antisymmetric_in the
carrier of c
1
by ORDERS_2:def 6;
E10:
c
2 is
finite
;
defpred S
1[
set ] means not ( a
1 <> {} & ( for b
1 being
Element of c
1 holds
not ( b
1 in a
1 & b
1 is_maximal_wrt a
1,the
InternalRel of c
1 ) ) );
E11:
S
1[
{} ]
;
now
let c
5, c
6 be
set ;
assume that E12:
( c
5 in c
2 & c
6 c= c
2 )
and E13:
not ( c
6 <> {} & ( for b
1 being
Element of c
1 holds
not ( b
1 in c
6 & b
1 is_maximal_wrt c
6,the
InternalRel of c
1 ) ) )
;
reconsider c
7 = c
5 as
Element of c
1 by E12;
assume
c
6 \/ {c5} <> {}
;
per cases
not ( not c
6 = {} & not c
6 <> {} )
;
suppose E14:
c
6 = {}
;
end;
suppose
c
6 <> {}
;
then consider c
8 being
Element of c
1 such that E14:
( c
8 in c
6 & c
8 is_maximal_wrt c
6,the
InternalRel of c
1 )
by E13;
now
per cases
not ( not
[c8,c5] in the
InternalRel of c
1 & not
[c5,c8] in the
InternalRel of c
1 & not ( not
[c8,c5] in the
InternalRel of c
1 & not
[c5,c8] in the
InternalRel of c
1 ) )
;
suppose E15:
[c8,c5] in the
InternalRel of c
1
;
take c
9 = c
7;
E16:
c
5 in {c5}
by TARSKI:def 1;
hence
c
9 in c
6 \/ {c5}
by XBOOLE_0:def 2;
now
thus
c
9 in c
6 \/ {c5}
by E16, XBOOLE_0:def 2;
now
assume
ex b
1 being
set st
( b
1 in c
6 \/ {c5} & b
1 <> c
5 &
[c5,b1] in the
InternalRel of c
1 )
;
then consider c
10 being
set such that E17:
( c
10 in c
6 \/ {c5} & c
10 <> c
5 &
[c5,c10] in the
InternalRel of c
1 )
;
( c
8 in the
carrier of c
1 & c
9 in the
carrier of c
1 & c
10 in the
carrier of c
1 )
by E17, ZFMISC_1:106;
then E18:
[c8,c10] in the
InternalRel of c
1
by E8, E15, E17, RELAT_2:def 8;
per cases
( c
10 in c
6 or c
10 in {c5} )
by E17, XBOOLE_0:def 2;
suppose E19:
c
10 in c
6
;
now
per cases
not ( not c
10 = c
8 & not c
10 <> c
8 )
;
suppose E20:
c
10 = c
8
;
then
c
8 = c
9
by E9, E15, E17, RELAT_2:def 4;
hence
not verum
by E17, E20;
end;
end;
hence
not verum
;
end;
suppose
c
10 in {c5}
;
end;
end;
end;
hence
for b
1 being
set holds
not ( b
1 in c
6 \/ {c5} & b
1 <> c
5 &
[c5,b1] in the
InternalRel of c
1 )
;
end;
hence
c
9 is_maximal_wrt c
6 \/ {c5},the
InternalRel of c
1
by WAYBEL_4:def 24;
end;
end;
hence
ex b
1 being
Element of c
1 st
( b
1 in c
6 \/ {c5} & b
1 is_maximal_wrt c
6 \/ {c5},the
InternalRel of c
1 )
;
end;
end;
end;
then E12:
for b
1, b
2 being
set holds
( ( b
1 in c
2 & b
2 c= c
2 & S
1[b
2] ) implies ( S
1[b
2 \/ {b1}] ) )
;
thus
S
1[c
2]
from FINSET_1:sch 2(E10, E11, E12);
end;
theorem E8: :: BAGORDER:8
proof
let c
1 be non
empty transitive antisymmetric RelStr ;
let c
2 be
finite Subset of c
1;
set c
3 = the
InternalRel of c
1;
set c
4 = the
carrier of c
1;
E9:
the
InternalRel of c
1 is_transitive_in the
carrier of c
1
by ORDERS_2:def 5;
E10:
the
InternalRel of c
1 is_antisymmetric_in the
carrier of c
1
by ORDERS_2:def 6;
E11:
c
2 is
finite
;
defpred S
1[
set ] means not ( a
1 <> {} & ( for b
1 being
Element of c
1 holds
not ( b
1 in a
1 & b
1 is_minimal_wrt a
1,the
InternalRel of c
1 ) ) );
E12:
S
1[
{} ]
;
now
let c
5, c
6 be
set ;
assume that E13:
( c
5 in c
2 & c
6 c= c
2 )
and E14:
not ( c
6 <> {} & ( for b
1 being
Element of c
1 holds
not ( b
1 in c
6 & b
1 is_minimal_wrt c
6,the
InternalRel of c
1 ) ) )
;
reconsider c
7 = c
5 as
Element of c
1 by E13;
assume
c
6 \/ {c5} <> {}
;
per cases
not ( not c
6 = {} & not c
6 <> {} )
;
suppose E15:
c
6 = {}
;
end;
suppose
c
6 <> {}
;
then consider c
8 being
Element of c
1 such that E15:
( c
8 in c
6 & c
8 is_minimal_wrt c
6,the
InternalRel of c
1 )
by E14;
now
per cases
not ( not
[c5,c8] in the
InternalRel of c
1 & not
[c8,c5] in the
InternalRel of c
1 & not ( not
[c8,c5] in the
InternalRel of c
1 & not
[c5,c8] in the
InternalRel of c
1 ) )
;
suppose E16:
[c5,c8] in the
InternalRel of c
1
;
take c
9 = c
7;
E17:
c
5 in {c5}
by TARSKI:def 1;
hence
c
9 in c
6 \/ {c5}
by XBOOLE_0:def 2;
now
thus
c
9 in c
6 \/ {c5}
by E17, XBOOLE_0:def 2;
now
assume
ex b
1 being
set st
( b
1 in c
6 \/ {c5} & b
1 <> c
5 &
[b1,c5] in the
InternalRel of c
1 )
;
then consider c
10 being
set such that E18:
( c
10 in c
6 \/ {c5} & c
10 <> c
5 &
[c10,c5] in the
InternalRel of c
1 )
;
( c
8 in the
carrier of c
1 & c
9 in the
carrier of c
1 & c
10 in the
carrier of c
1 )
by E18, ZFMISC_1:106;
then E19:
[c10,c8] in the
InternalRel of c
1
by E9, E16, E18, RELAT_2:def 8;
per cases
( c
10 in c
6 or c
10 in {c5} )
by E18, XBOOLE_0:def 2;
suppose E20:
c
10 in c
6
;
now
per cases
not ( not c
10 = c
8 & not c
10 <> c
8 )
;
suppose E21:
c
10 = c
8
;
then
c
8 = c
9
by E10, E16, E18, RELAT_2:def 4;
hence
not verum
by E18, E21;
end;
end;
hence
not verum
;
end;
suppose
c
10 in {c5}
;
end;
end;
end;
hence
for b
1 being
set holds
not ( b
1 in c
6 \/ {c5} & b
1 <> c
5 &
[b1,c5] in the
InternalRel of c
1 )
;
end;
hence
c
9 is_minimal_wrt c
6 \/ {c5},the
InternalRel of c
1
by WAYBEL_4:def 26;
end;
end;
hence
ex b
1 being
Element of c
1 st
( b
1 in c
6 \/ {c5} & b
1 is_minimal_wrt c
6 \/ {c5},the
InternalRel of c
1 )
;
end;
end;
end;
then E13:
for b
1, b
2 being
set holds
( ( b
1 in c
2 & b
2 c= c
2 & S
1[b
2] ) implies ( S
1[b
2 \/ {b1}] ) )
;
thus
S
1[c
2]
from FINSET_1:sch 2(E11, E12, E13);
end;
theorem :: BAGORDER:9
:: deftheorem E9 defines non-increasing BAGORDER:def 3 :
theorem E10: :: BAGORDER:10