let E be non empty set ; :: thesis: for f being Function of E,E st f is without_fixpoints holds
ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
let f be Function of E,E; :: thesis: ( f is without_fixpoints implies ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 ) )
defpred S1[ set , Element of [:(bool E),(bool E),(bool E):]] means ( (($2 `1_3) \/ ($2 `2_3)) \/ ($2 `3_3) = $1 & f .: ($2 `1_3) misses $2 `1_3 & f .: ($2 `2_3) misses $2 `2_3 & f .: ($2 `3_3) misses $2 `3_3 );
deffunc H1( Nat) -> Function of E,E = iter (f,$1);
assume A1: f is without_fixpoints ; :: thesis: ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
A2: for a being Element of Class (=_ f) ex b being Element of [:(bool E),(bool E),(bool E):] st S1[a,b]
proof
reconsider c3 = {} as Subset of E by XBOOLE_1:2;
let c be Element of Class (=_ f); :: thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
consider x0 being object such that
A3: x0 in E and
A4: c = Class ((=_ f),x0) by EQREL_1:def 3;
reconsider x0 = x0 as Element of c by A3, A4, EQREL_1:20;
defpred S2[ set ] means ex k, l being Nat st
( H1(k) . $1 = H1(l) . x0 & k is even & l is even );
set c1 = { x where x is Element of c : S2[x] } ;
{ x where x is Element of c : S2[x] } is Subset of c from DOMAIN_1:sch 7();
 then reconsider c1 = { x where x is Element of c : S2[x] } as Subset of E by XBOOLE_1:1;
defpred S3[ set ] means ex k, l being Nat st
( H1(k) . $1 = H1(l) . x0 & k is odd & l is even );
set c2 = { x where x is Element of c : S3[x] } ;
{ x where x is Element of c : S3[x] } is Subset of c from DOMAIN_1:sch 7();
 then reconsider c2 = { x where x is Element of c : S3[x] } as Subset of E by XBOOLE_1:1;
per cases ( c1 misses c2 or c1 meets c2 ) ;
suppose A5: c1 misses c2 ; :: thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
take b = [c1,c2,c3]; :: thesis: S1[c,b]
A6: b `2_3 = c2 by MCART_1:def 6;
A7: b `3_3 = c3 by MCART_1:def 7;
A8: b `1_3 = c1 by MCART_1:def 5;
thus ((b `1_3) \/ (b `2_3)) \/ (b `3_3) = c :: thesis: ( f .: (b `1_3) misses b `1_3 & f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: c c= ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
let x be object ; :: thesis: ( x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) implies b1 in c )
assume A9: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) ; :: thesis: b1 in c
per cases ( x in c1 or x in c2 or x in c3 ) by A8, A6, A7, A9, XBOOLE_0:def 3;
suppose x in c1 ; :: thesis: b1 in c
then ex xx being Element of c st
( x = xx & ex k, l being Nat st
( H1(k) . xx = H1(l) . x0 & k is even & l is even ) ) ;
hence x in c ; :: thesis: verum
end;
suppose x in c2 ; :: thesis: b1 in c
then ex xx being Element of c st
( x = xx & ex k, l being Nat st
( H1(k) . xx = H1(l) . x0 & k is odd & l is even ) ) ;
hence x in c ; :: thesis: verum
end;
suppose x in c3 ; :: thesis: b1 in c
hence x in c ; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in c or x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) )
assume x in c ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider xc = x as Element of c ;
[xc,x0] in =_ f by A4, EQREL_1:19;
then consider k, l being Nat such that
A10: H1(k) . xc = H1(l) . x0 by Def7;
A11: dom H1(l) = E by FUNCT_2:def 1;
A12: dom H1(k) = E by FUNCT_2:def 1;
per cases ( k is even or k is odd ) ;
suppose A13: k is even ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider k = k as even Nat ;
thus x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) :: thesis: verum
proof
per cases ( l is even or l is odd ) ;
suppose l is even ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then xc in c1 by A10, A13;
hence x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A8, A7, XBOOLE_0:def 3; :: thesis: verum
end;
suppose l is odd ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider l = l as odd Nat ;
H1(k + 1) . xc = (f * H1(k)) . xc by FUNCT_7:71
.= f . (H1(l) . x0) by A10, A12, FUNCT_1:13
.= (f * H1(l)) . x0 by A11, FUNCT_1:13
.= H1(l + 1) . x0 by FUNCT_7:71 ;
then xc in c2 ;
hence x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A6, A7, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
end;
suppose A14: k is odd ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider k = k as odd Nat ;
thus x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) :: thesis: verum
proof
per cases ( l is even or l is odd ) ;
suppose l is even ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then xc in c2 by A10, A14;
hence x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A6, A7, XBOOLE_0:def 3; :: thesis: verum
end;
suppose l is odd ; :: thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider l = l as odd Nat ;
H1(k + 1) . xc = (f * H1(k)) . xc by FUNCT_7:71
.= f . (H1(l) . x0) by A10, A12, FUNCT_1:13
.= (f * H1(l)) . x0 by A11, FUNCT_1:13
.= H1(l + 1) . x0 by FUNCT_7:71 ;
then xc in c1 ;
hence x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A8, A7, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
end;
end;
end;
f .: c1 c= c2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: c1 or y in c2 )
A15: dom f = E by FUNCT_2:def 1;
assume y in f .: c1 ; :: thesis: y in c2
then consider x being object such that
x in dom f and
A16: x in c1 and
A17: y = f . x by FUNCT_1:def 6;
consider xx being Element of c such that
A18: x = xx and
A19: ex k, l being Nat st
( H1(k) . xx = H1(l) . x0 & k is even & l is even ) by A16;
consider k, l being Nat such that
A20: H1(k) . xx = H1(l) . x0 and
A21: ( k is even & l is even ) by A19;
reconsider k = k, l = l as even Nat by A21;
reconsider k1 = k + 1 as odd Element of NAT ;
reconsider l1 = l + 1 as odd Element of NAT ;
reconsider l2 = l1 + 1 as even Element of NAT ;
A22: dom H1(k) = E by FUNCT_2:def 1;
reconsider yc = y as Element of c by A17, A18, Th6;
A23: dom H1(l) = E by FUNCT_2:def 1;
A24: dom H1(k1) = E by FUNCT_2:def 1;
A25: H1(k1 + 1) . xx = (H1(k1) * f) . xx by FUNCT_7:69
.= H1(k1) . (f . xx) by A15, FUNCT_1:13 ;
A26: dom H1(l1) = E by FUNCT_2:def 1;
H1(k1 + 1) . xx = (f * H1(k1)) . xx by FUNCT_7:71
.= f . (H1(k1) . xx) by A24, FUNCT_1:13
.= f . ((f * H1(k)) . xx) by FUNCT_7:71
.= f . (f . (H1(l) . x0)) by A20, A22, FUNCT_1:13
.= f . ((f * H1(l)) . x0) by A23, FUNCT_1:13
.= f . (H1(l1) . x0) by FUNCT_7:71
.= (f * H1(l1)) . x0 by A26, FUNCT_1:13
.= H1(l2) . x0 by FUNCT_7:71 ;
then yc in c2 by A17, A18, A25;
hence y in c2 ; :: thesis: verum
end;
hence f .: (b `1_3) misses b `1_3 by A5, A8, XBOOLE_1:63; :: thesis: ( f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
f .: c2 c= c1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: c2 or y in c1 )
A27: dom f = E by FUNCT_2:def 1;
assume y in f .: c2 ; :: thesis: y in c1
then consider x being object such that
x in dom f and
A28: x in c2 and
A29: y = f . x by FUNCT_1:def 6;
consider xx being Element of c such that
A30: x = xx and
A31: ex k, l being Nat st
( H1(k) . xx = H1(l) . x0 & k is odd & l is even ) by A28;
consider k, l being Nat such that
A32: H1(k) . xx = H1(l) . x0 and
A33: k is odd and
A34: l is even by A31;
reconsider l = l as even Nat by A34;
reconsider k = k as odd Nat by A33;
reconsider k1 = k + 1 as even Element of NAT ;
reconsider l1 = l + 1 as odd Element of NAT ;
reconsider l2 = l1 + 1 as even Element of NAT ;
A35: dom H1(k) = E by FUNCT_2:def 1;
reconsider yc = y as Element of c by A29, A30, Th6;
A36: dom H1(l) = E by FUNCT_2:def 1;
A37: dom H1(k1) = E by FUNCT_2:def 1;
A38: H1(k1 + 1) . xx = (H1(k1) * f) . xx by FUNCT_7:69
.= H1(k1) . (f . xx) by A27, FUNCT_1:13 ;
A39: dom H1(l1) = E by FUNCT_2:def 1;
H1(k1 + 1) . xx = (f * H1(k1)) . xx by FUNCT_7:71
.= f . (H1(k1) . xx) by A37, FUNCT_1:13
.= f . ((f * H1(k)) . xx) by FUNCT_7:71
.= f . (f . (H1(l) . x0)) by A32, A35, FUNCT_1:13
.= f . ((f * H1(l)) . x0) by A36, FUNCT_1:13
.= f . (H1(l1) . x0) by FUNCT_7:71
.= (f * H1(l1)) . x0 by A39, FUNCT_1:13
.= H1(l2) . x0 by FUNCT_7:71 ;
then yc in c1 by A29, A30, A38;
hence y in c1 ; :: thesis: verum
end;
hence f .: (b `2_3) misses b `2_3 by A5, A6, XBOOLE_1:63; :: thesis: f .: (b `3_3) misses b `3_3
thus f .: (b `3_3) misses b `3_3 by A7; :: thesis: verum
end;
suppose c1 meets c2 ; :: thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
then consider x1 being object such that
A40: x1 in c1 and
A41: x1 in c2 by XBOOLE_0:3;
consider x11 being Element of c such that
A42: x1 = x11 and
A43: ex k, l being Nat st
( H1(k) . x11 = H1(l) . x0 & k is even & l is even ) by A40;
consider x12 being Element of c such that
A44: x1 = x12 and
A45: ex k, l being Nat st
( H1(k) . x12 = H1(l) . x0 & k is odd & l is even ) by A41;
consider k2, l2 being Nat such that
A46: H1(k2) . x12 = H1(l2) . x0 and
A47: k2 is odd and
A48: l2 is even by A45;
reconsider x1 = x1 as Element of c by A42;
consider k1, l1 being Nat such that
A49: H1(k1) . x11 = H1(l1) . x0 and
A50: ( k1 is even & l1 is even ) by A43;
A51: dom H1(k1) = E by FUNCT_2:def 1;
A52: dom H1(l1) = E by FUNCT_2:def 1;
A53: H1(l2 + k1) . x1 = (H1(l2) * H1(k1)) . x1 by FUNCT_7:77
.= H1(l2) . (H1(l1) . x0) by A42, A49, A51, FUNCT_1:13
.= (H1(l2) * H1(l1)) . x0 by A52, FUNCT_1:13
.= H1(l1 + l2) . x0 by FUNCT_7:77 ;
A54: dom H1(l2) = E by FUNCT_2:def 1;
A55: dom H1(k2) = E by FUNCT_2:def 1;
A56: H1(l1 + k2) . x1 = (H1(l1) * H1(k2)) . x1 by FUNCT_7:77
.= H1(l1) . (H1(l2) . x0) by A44, A46, A55, FUNCT_1:13
.= (H1(l1) * H1(l2)) . x0 by A54, FUNCT_1:13
.= H1(l1 + l2) . x0 by FUNCT_7:77 ;
ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
proof
reconsider k2 = k2 as odd Nat by A47;
reconsider k1 = k1, l1 = l1, l2 = l2 as even Nat by A50, A48;
A57: dom H1(k1 + l2) = E by FUNCT_2:def 1;
A58: dom H1(k2 + l1) = E by FUNCT_2:def 1;
per cases ( k1 + l2 < k2 + l1 or k1 + l2 > k2 + l1 ) by XXREAL_0:1;
suppose k1 + l2 < k2 + l1 ; :: thesis: ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
then reconsider k = (k2 + l1) - (k1 + l2) as Element of NAT by INT_1:5;
take r = H1(k1 + l2) . x1; :: thesis: ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
reconsider k = k as odd Element of NAT ;
take k ; :: thesis: ( H1(k) . r = r & r in c )
H1(k) . (H1(k1 + l2) . x1) = (H1(k) * H1(k1 + l2)) . x1 by A57, FUNCT_1:13
.= H1(k + (k1 + l2)) . x1 by FUNCT_7:77
.= H1(k1 + l2) . x1 by A56, A53 ;
hence H1(k) . r = r ; :: thesis: r in c
thus r in c by Th7; :: thesis: verum
end;
suppose k1 + l2 > k2 + l1 ; :: thesis: ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
then reconsider k = (k1 + l2) - (k2 + l1) as Element of NAT by INT_1:5;
take r = H1(k2 + l1) . x1; :: thesis: ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
reconsider k = k as odd Element of NAT ;
take k ; :: thesis: ( H1(k) . r = r & r in c )
H1(k) . (H1(k2 + l1) . x1) = (H1(k) * H1(k2 + l1)) . x1 by A58, FUNCT_1:13
.= H1(k + (k2 + l1)) . x1 by FUNCT_7:77
.= H1(k2 + l1) . x1 by A56, A53 ;
hence H1(k) . r = r ; :: thesis: r in c
thus r in c by Th7; :: thesis: verum
end;
end;
end;
then consider r being Element of E, k being odd Element of NAT such that
A59: H1(k) . r = r and
A60: r in c ;
reconsider r = r as Element of c by A60;
deffunc H2( set ) -> set = { l where l is Element of NAT : H1(l) . $1 = r } ;
A61: for x being Element of c holds H2(x) in bool NAT
proof
let x be Element of c; :: thesis: H2(x) in bool NAT
defpred S4[ Element of NAT ] means H1($1) . x = r;
{ l where l is Element of NAT : S4[l] } is Subset of NAT from DOMAIN_1:sch 7();
 hence H2(x) in bool NAT ; :: thesis: verum
end;
consider Odl being Function of c,(bool NAT) such that
A62: for x being Element of c holds Odl . x = H2(x) from FUNCT_2:sch 8(A61);
now :: thesis: for n being object st n in dom Odl holds
not Odl . n is empty
defpred S4[ Nat] means H1(k * $1) . r = r;
let n be object ; :: thesis: ( n in dom Odl implies not Odl . n is empty )
assume n in dom Odl ; :: thesis: not Odl . n is empty
then reconsider nc = n as Element of c by FUNCT_2:def 1;
A63: Odl . nc = { l where l is Element of NAT : H1(l) . nc = r } by A62;
A64: now :: thesis: for i being Nat st S4[i] holds
S4[i + 1]
let i be Nat; :: thesis: ( S4[i] implies S4[i + 1] )
assume A65: S4[i] ; :: thesis: S4[i + 1]
A66: dom H1(k) = E by FUNCT_2:def 1;
H1(k * (i + 1)) . r = H1((k * i) + (k * 1)) . r
.= (H1(k * i) * H1(k)) . r by FUNCT_7:77
.= r by A59, A65, A66, FUNCT_1:13 ;
hence S4[i + 1] ; :: thesis: verum
end;
A67: S4[ 0 ] by Th3;
A68: for i being Nat holds S4[i] from NAT_1:sch 2(A67, A64);
 ex x9 being object st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def 3;
then [nc,r] in =_ f by EQREL_1:22;
then consider kn, ln being Nat such that
A69: (iter (f,kn)) . nc = (iter (f,ln)) . r by Def7;
A70: dom H1(ln) = E by FUNCT_2:def 1;
set mk = ln mod k;
set dk = ln div k;
A71: dom H1(kn) = E by FUNCT_2:def 1;
A72: 2 * 0 <> k ;
then ln mod k < k by NAT_D:1;
then reconsider kmk = k - (ln mod k) as Element of NAT by INT_1:5;
ln = (k * (ln div k)) + (ln mod k) by A72, NAT_D:2;
then A73: ln + kmk = k * ((ln div k) + 1) ;
H1(kmk + kn) . nc = (H1(kmk) * H1(kn)) . nc by FUNCT_7:77
.= H1(kmk) . (H1(ln) . r) by A69, A71, FUNCT_1:13
.= (H1(kmk) * H1(ln)) . r by A70, FUNCT_1:13
.= H1(k * ((ln div k) + 1)) . r by A73, FUNCT_7:77
.= r by A68 ;
then kn + kmk in Odl . n by A63;
hence not Odl . n is empty ; :: thesis: verum
end;
then reconsider Odl = Odl as non-empty Function of c,(bool NAT) by FUNCT_1:def 9;
deffunc H3( Element of c) -> Element of NAT = min (Odl . $1);
consider odl being Function of c,NAT such that
A74: for x being Element of c holds odl . x = H3(x) from FUNCT_2:sch 4();
defpred S4[ Element of c] means odl . $1 is even ;
set c1 = { x where x is Element of c : S4[x] } ;
set d1 = { x where x is Element of c : S4[x] } \ {r};
{ x where x is Element of c : S4[x] } is Subset of c from DOMAIN_1:sch 7();
then A75: { x where x is Element of c : S4[x] } \ {r} c= c by XBOOLE_1:1;
H1( 0 ) . r = r by Th3;
then 0 in { l where l is Element of NAT : H1(l) . r = r } ;
then 0 in Odl . r by A62;
then min (Odl . r) = 0 by Th2;
then A76: odl . r = 2 * 0 by A74;
then A77: r in { x where x is Element of c : S4[x] } ;
reconsider d1 = { x where x is Element of c : S4[x] } \ {r} as Subset of E by A75, XBOOLE_1:1;
defpred S5[ Element of c] means odl . $1 is odd ;
set d2 = { x where x is Element of c : S5[x] } ;
{ x where x is Element of c : S5[x] } is Subset of c from DOMAIN_1:sch 7();
then reconsider d2 = { x where x is Element of c : S5[x] } as Subset of E by XBOOLE_1:1;
A78: for x being Element of c st x <> r holds
odl . (f . x) = (odl . x) - 1
proof
let x be Element of c; :: thesis: ( x <> r implies odl . (f . x) = (odl . x) - 1 )
reconsider fx = f . x as Element of c by Th6;
reconsider ofx = odl . fx, ox = odl . x as Element of NAT ;
assume A79: x <> r ; :: thesis: odl . (f . x) = (odl . x) - 1
now :: thesis: not odl . x = 0
assume odl . x = 0 ; :: thesis: contradiction
then 0 = min (Odl . x) by A74;
then 0 in Odl . x by XXREAL_2:def 7;
then 0 in { l where l is Element of NAT : H1(l) . x = r } by A62;
then ex l being Element of NAT st
( l = 0 & H1(l) . x = r ) ;
hence contradiction by A79, Th3; :: thesis: verum
end;
then reconsider ox1 = ox - 1 as Element of NAT by INT_1:5, NAT_1:14;
ox = min (Odl . x) by A74;
then ox in Odl . x by XXREAL_2:def 7;
then ox in { l where l is Element of NAT : H1(l) . x = r } by A62;
then A80: ex l being Element of NAT st
( l = ox & H1(l) . x = r ) ;
A81: dom f = E by FUNCT_2:def 1;
then H1(ox1) . fx = (H1(ox1) * f) . x by FUNCT_1:13
.= H1(ox1 + 1) . x by FUNCT_7:69
.= H1(ox) . x ;
then ox1 in { l where l is Element of NAT : H1(l) . fx = r } by A80;
then A82: ox1 in Odl . fx by A62;
ofx = min (Odl . fx) by A74;
then ofx in Odl . fx by XXREAL_2:def 7;
then ofx in { l where l is Element of NAT : H1(l) . fx = r } by A62;
then A83: ex l being Element of NAT st
( l = ofx & H1(l) . fx = r ) ;
H1(ofx + 1) . x = (H1(ofx) * f) . x by FUNCT_7:69
.= H1(ofx) . fx by A81, FUNCT_1:13 ;
then ofx + 1 in { l where l is Element of NAT : H1(l) . x = r } by A83;
then A84: ofx + 1 in Odl . x by A62;
ox = min (Odl . x) by A74;
then ofx + 1 >= ox by A84, XXREAL_2:def 7;
then A85: ofx >= ox - 1 by XREAL_1:20;
ofx = min (Odl . fx) by A74;
then ofx <= ox - 1 by A82, XXREAL_2:def 7;
hence odl . (f . x) = (odl . x) - 1 by A85, XXREAL_0:1; :: thesis: verum
end;
A86: f .: d1 c= d2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: d1 or y in d2 )
assume y in f .: d1 ; :: thesis: y in d2
then consider x being object such that
x in dom f and
A87: x in d1 and
A88: y = f . x by FUNCT_1:def 6;
x in { x where x is Element of c : S4[x] } by A87;
then consider xx being Element of c such that
A89: x = xx and
A90: odl . xx is even ;
reconsider ox = odl . xx as even Element of NAT by A90;
reconsider yc = y as Element of c by A88, A89, Th6;
r <> xx by A87, A89, ZFMISC_1:56;
then odl . yc = ox - 1 by A78, A88, A89;
hence y in d2 ; :: thesis: verum
end;
A91: { x where x is Element of c : S4[x] } \/ d2 = c
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: c c= { x where x is Element of c : S4[x] } \/ d2
let x be object ; :: thesis: ( x in { x where x is Element of c : S4[x] } \/ d2 implies b1 in c )
assume A92: x in { x where x is Element of c : S4[x] } \/ d2 ; :: thesis: b1 in c
per cases ( x in { x where x is Element of c : S4[x] } or x in d2 ) by A92, XBOOLE_0:def 3;
suppose x in { x where x is Element of c : S4[x] } ; :: thesis: b1 in c
then ex xc being Element of c st
( xc = x & odl . xc is even ) ;
hence x in c ; :: thesis: verum
end;
suppose x in d2 ; :: thesis: b1 in c
then ex xc being Element of c st
( xc = x & odl . xc is odd ) ;
hence x in c ; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in c or x in { x where x is Element of c : S4[x] } \/ d2 )
assume x in c ; :: thesis: x in { x where x is Element of c : S4[x] } \/ d2
then reconsider xc = x as Element of c ;
( odl . xc is even or odl . xc is odd ) ;
then ( x in { x where x is Element of c : S4[x] } or x in d2 ) ;
hence x in { x where x is Element of c : S4[x] } \/ d2 by XBOOLE_0:def 3; :: thesis: verum
end;
reconsider d3 = {r} as Subset of E by ZFMISC_1:31;
take b = [d1,d2,d3]; :: thesis: S1[c,b]
A93: b `1_3 = d1 by MCART_1:def 5;
A94: b `2_3 = d2 by MCART_1:def 6;
A95: b `3_3 = d3 by MCART_1:def 7;
d1 \/ d3 = { x where x is Element of c : S4[x] } \/ d3 by XBOOLE_1:39
.= { x where x is Element of c : S4[x] } by A77, ZFMISC_1:40 ;
hence ((b `1_3) \/ (b `2_3)) \/ (b `3_3) = c by A93, A94, A95, A91, XBOOLE_1:4; :: thesis: ( f .: (b `1_3) misses b `1_3 & f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
A96: { x where x is Element of c : S4[x] } misses d2
proof
assume { x where x is Element of c : S4[x] } meets d2 ; :: thesis: contradiction
then consider z being object such that
A97: ( z in { x where x is Element of c : S4[x] } & z in d2 ) by XBOOLE_0:3;
( ex x being Element of c st
( z = x & odl . x is even ) & ex x being Element of c st
( z = x & odl . x is odd ) ) by A97;
hence contradiction ; :: thesis: verum
end;
then d1 misses d2 by XBOOLE_1:63;
hence f .: (b `1_3) misses b `1_3 by A93, A86, XBOOLE_1:63; :: thesis: ( f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
f .: d2 c= { x where x is Element of c : S4[x] }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: d2 or y in { x where x is Element of c : S4[x] } )
assume y in f .: d2 ; :: thesis: y in { x where x is Element of c : S4[x] }
then consider x being object such that
x in dom f and
A98: x in d2 and
A99: y = f . x by FUNCT_1:def 6;
consider xx being Element of c such that
A100: x = xx and
A101: odl . xx is odd by A98;
reconsider ox = odl . xx as odd Element of NAT by A101;
reconsider yc = y as Element of c by A99, A100, Th6;
odl . yc = ox - 1 by A76, A78, A99, A100;
hence y in { x where x is Element of c : S4[x] } ; :: thesis: verum
end;
hence f .: (b `2_3) misses b `2_3 by A94, A96, XBOOLE_1:63; :: thesis: f .: (b `3_3) misses b `3_3
thus f .: (b `3_3) misses b `3_3 :: thesis: verum
proof
assume f .: (b `3_3) meets b `3_3 ; :: thesis: contradiction
then consider y being object such that
A102: y in f .: (b `3_3) and
A103: y in b `3_3 by XBOOLE_0:3;
A104: y = r by A95, A103, TARSKI:def 1;
consider x being object such that
x in dom f and
A105: x in {r} and
A106: y = f . x by A95, A102, FUNCT_1:def 6;
x = r by A105, TARSKI:def 1;
then r is_a_fixpoint_of f by A104, A106;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
end;
consider F being Function of (Class (=_ f)),[:(bool E),(bool E),(bool E):] such that
A107: for a being Element of Class (=_ f) holds S1[a,F . a] from FUNCT_2:sch 3(A2);
 set E3c = { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ;
set E2c = { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ;
set E1c = { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ;
set E1 = union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ;
set E2 = union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ;
set E3 = union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ;
take union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ; :: thesis: ex E2, E3 being set st
( ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ E2) \/ E3 = E & f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } & f .: E2 misses E2 & f .: E3 misses E3 )
take union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ; :: thesis: ex E3 being set st
( ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ E3 = E & f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } & f .: E3 misses E3 )
take union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ; :: thesis: ( ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) = E & f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
thus ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) = E :: thesis: ( f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: E c= ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
let x be object ; :: thesis: ( x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) implies b1 in E )
assume x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) ; :: thesis: b1 in E
then A108: ( x in (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) or x in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3;
per cases ( x in union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } or x in union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } or x in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) by A108, XBOOLE_0:def 3;
suppose x in union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ; :: thesis: b1 in E
then consider Y being set such that
A109: x in Y and
A110: Y in { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } by TARSKI:def 4;
ex c being Element of Class (=_ f) st Y = (F . c) `1_3 by A110;
hence x in E by A109; :: thesis: verum
end;
suppose x in union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ; :: thesis: b1 in E
then consider Y being set such that
A111: x in Y and
A112: Y in { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } by TARSKI:def 4;
ex c being Element of Class (=_ f) st Y = (F . c) `2_3 by A112;
hence x in E by A111; :: thesis: verum
end;
suppose x in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ; :: thesis: b1 in E
then consider Y being set such that
A113: x in Y and
A114: Y in { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } by TARSKI:def 4;
ex c being Element of Class (=_ f) st Y = (F . c) `3_3 by A114;
hence x in E by A113; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E or x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) )
set c = Class ((=_ f),x);
assume A115: x in E ; :: thesis: x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
then A116: x in Class ((=_ f),x) by EQREL_1:20;
reconsider c = Class ((=_ f),x) as Element of Class (=_ f) by A115, EQREL_1:def 3;
x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by A107, A116;
then A117: ( x in ((F . c) `1_3) \/ ((F . c) `2_3) or x in (F . c) `3_3 ) by XBOOLE_0:def 3;
per cases ( x in (F . c) `1_3 or x in (F . c) `2_3 or x in (F . c) `3_3 ) by A117, XBOOLE_0:def 3;
suppose A118: x in (F . c) `1_3 ; :: thesis: x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
(F . c) `1_3 in { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ;
then x in union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } by A118, TARSKI:def 4;
then x in (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3;
hence x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A119: x in (F . c) `2_3 ; :: thesis: x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
(F . c) `2_3 in { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ;
then x in union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } by A119, TARSKI:def 4;
then x in (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3;
hence x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A120: x in (F . c) `3_3 ; :: thesis: x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
(F . c) `3_3 in { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ;
then x in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } by A120, TARSKI:def 4;
hence x in ((union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
thus f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } :: thesis: ( f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } )
proof
assume not f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ; :: thesis: contradiction
then consider x being object such that
A121: x in f .: (union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } ) and
A122: x in union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } by XBOOLE_0:3;
consider Y being set such that
A123: x in Y and
A124: Y in { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } by A122, TARSKI:def 4;
consider c being Element of Class (=_ f) such that
A125: Y = (F . c) `1_3 by A124;
x in ((F . c) `1_3) \/ ((F . c) `2_3) by A123, A125, XBOOLE_0:def 3;
then x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by XBOOLE_0:def 3;
then A126: x in c by A107;
ex x9 being object st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def 3;
then A127: c = Class ((=_ f),x) by A126, EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then A128: x in (dom f) \/ (rng f) by A123, A125, XBOOLE_0:def 3;
consider xx being object such that
A129: xx in dom f and
A130: xx in union { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } and
A131: x = f . xx by A121, FUNCT_1:def 6;
consider YY being set such that
A132: xx in YY and
A133: YY in { ((F . c) `1_3) where c is Element of Class (=_ f) : verum } by A130, TARSKI:def 4;
consider cc being Element of Class (=_ f) such that
A134: YY = (F . cc) `1_3 by A133;
xx in ((F . cc) `1_3) \/ ((F . cc) `2_3) by A132, A134, XBOOLE_0:def 3;
then xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by XBOOLE_0:def 3;
then A135: xx in cc by A107;
ex xx9 being object st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def 3;
then A136: cc = Class ((=_ f),xx) by A135, EQREL_1:23;
(iter (f,1)) . xx = x by A131, FUNCT_7:70
.= (id (field f)) . x by A128, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then [x,xx] in =_ f by A123, A125, A132, A134, Def7;
then A137: Class ((=_ f),x) = Class ((=_ f),xx) by A123, A125, EQREL_1:35;
A138: f . xx in f .: YY by A129, A132, FUNCT_1:def 6;
f .: YY misses YY by A107, A134;
hence contradiction by A123, A125, A131, A134, A127, A136, A137, A138, XBOOLE_0:3; :: thesis: verum
end;
thus f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } :: thesis: f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum }
proof
assume not f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ; :: thesis: contradiction
then consider x being object such that
A139: x in f .: (union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } ) and
A140: x in union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } by XBOOLE_0:3;
consider Y being set such that
A141: x in Y and
A142: Y in { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } by A140, TARSKI:def 4;
consider c being Element of Class (=_ f) such that
A143: Y = (F . c) `2_3 by A142;
x in ((F . c) `1_3) \/ ((F . c) `2_3) by A141, A143, XBOOLE_0:def 3;
then x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by XBOOLE_0:def 3;
then A144: x in c by A107;
ex x9 being object st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def 3;
then A145: c = Class ((=_ f),x) by A144, EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then A146: x in (dom f) \/ (rng f) by A141, A143, XBOOLE_0:def 3;
consider xx being object such that
A147: xx in dom f and
A148: xx in union { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } and
A149: x = f . xx by A139, FUNCT_1:def 6;
consider YY being set such that
A150: xx in YY and
A151: YY in { ((F . c) `2_3) where c is Element of Class (=_ f) : verum } by A148, TARSKI:def 4;
consider cc being Element of Class (=_ f) such that
A152: YY = (F . cc) `2_3 by A151;
xx in ((F . cc) `1_3) \/ ((F . cc) `2_3) by A150, A152, XBOOLE_0:def 3;
then xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by XBOOLE_0:def 3;
then A153: xx in cc by A107;
ex xx9 being object st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def 3;
then A154: cc = Class ((=_ f),xx) by A153, EQREL_1:23;
(iter (f,1)) . xx = x by A149, FUNCT_7:70
.= (id (field f)) . x by A146, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then [x,xx] in =_ f by A141, A143, A150, A152, Def7;
then A155: Class ((=_ f),x) = Class ((=_ f),xx) by A141, A143, EQREL_1:35;
A156: f . xx in f .: YY by A147, A150, FUNCT_1:def 6;
f .: YY misses YY by A107, A152;
hence contradiction by A141, A143, A149, A152, A145, A154, A155, A156, XBOOLE_0:3; :: thesis: verum
end;
thus f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } :: thesis: verum
proof
assume not f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ; :: thesis: contradiction
then consider x being object such that
A157: x in f .: (union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } ) and
A158: x in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } by XBOOLE_0:3;
consider Y being set such that
A159: x in Y and
A160: Y in { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } by A158, TARSKI:def 4;
consider c being Element of Class (=_ f) such that
A161: Y = (F . c) `3_3 by A160;
x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by A159, A161, XBOOLE_0:def 3;
then A162: x in c by A107;
ex x9 being object st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def 3;
then A163: c = Class ((=_ f),x) by A162, EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then A164: x in (dom f) \/ (rng f) by A159, A161, XBOOLE_0:def 3;
consider xx being object such that
A165: xx in dom f and
A166: xx in union { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } and
A167: x = f . xx by A157, FUNCT_1:def 6;
consider YY being set such that
A168: xx in YY and
A169: YY in { ((F . c) `3_3) where c is Element of Class (=_ f) : verum } by A166, TARSKI:def 4;
consider cc being Element of Class (=_ f) such that
A170: YY = (F . cc) `3_3 by A169;
xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by A168, A170, XBOOLE_0:def 3;
then A171: xx in cc by A107;
ex xx9 being object st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def 3;
then A172: cc = Class ((=_ f),xx) by A171, EQREL_1:23;
(iter (f,1)) . xx = x by A167, FUNCT_7:70
.= (id (field f)) . x by A164, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then [x,xx] in =_ f by A159, A161, A168, A170, Def7;
then A173: Class ((=_ f),x) = Class ((=_ f),xx) by A159, A161, EQREL_1:35;
A174: f . xx in f .: YY by A165, A168, FUNCT_1:def 6;
f .: YY misses YY by A107, A170;
hence contradiction by A159, A161, A167, A170, A163, A172, A173, A174, XBOOLE_0:3; :: thesis: verum
end;