let E be non empty set ; :: thesis: for f being Function of E,E st f has_no_fixpoint 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 has_no_fixpoint implies ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 ) )
assume A1:
f has_no_fixpoint
; :: thesis: 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[ Element of Class (=_ f), Element of [:(bool E),(bool E),(bool E):]] means ( (($2 `1 ) \/ ($2 `2 )) \/ ($2 `3 ) = $1 & f .: ($2 `1 ) misses $2 `1 & f .: ($2 `2 ) misses $2 `2 & f .: ($2 `3 ) misses $2 `3 );
deffunc H1( Element of NAT ) -> Function of E,E = iter f,$1;
A2:
for a being Element of Class (=_ f) ex b being Element of [:(bool E),(bool E),(bool E):] st S1[a,b]
proof
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
set such that A3:
(
x0 in E &
c = Class (=_ f),
x0 )
by EQREL_1:def 5;
reconsider x0 =
x0 as
Element of
c by A3, EQREL_1:28;
defpred S2[
set ]
means ex
k,
l being
Element of
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
Element of
NAT st
(
H1(
k)
. $1
= H1(
l)
. x0 & not
k is
even &
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;
reconsider c3 =
{} as
Subset of
E by XBOOLE_1:2;
per cases
( c1 misses c2 or c1 meets c2 )
;
suppose A4:
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]A5:
(
b `1 = c1 &
b `2 = c2 &
b `3 = c3 )
by MCART_1:47;
thus
((b `1 ) \/ (b `2 )) \/ (b `3 ) = c
:: thesis: ( f .: (b `1 ) misses b `1 & f .: (b `2 ) misses b `2 & f .: (b `3 ) misses b `3 )thus
f .: (b `1 ) misses b `1
:: thesis: ( f .: (b `2 ) misses b `2 & f .: (b `3 ) misses b `3 )proof
f .: c1 c= c2
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in f .: c1 or y in c2 )
assume
y in f .: c1
;
:: thesis: y in c2
then consider x being
set such that A13:
(
x in dom f &
x in c1 &
y = f . x )
by FUNCT_1:def 12;
consider xx being
Element of
c such that A14:
(
x = xx & ex
k,
l being
Element of
NAT st
(
H1(
k)
. xx = H1(
l)
. x0 &
k is
even &
l is
even ) )
by A13;
reconsider yc =
y as
Element of
c by A13, A14, Th6;
consider k,
l being
Element of
NAT such that A15:
(
H1(
k)
. xx = H1(
l)
. x0 &
k is
even &
l is
even )
by A14;
reconsider k =
k,
l =
l as
even Element of
NAT by A15;
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 ;
A16:
(
dom f = E &
dom H1(
k)
= E &
dom H1(
l)
= E &
dom H1(
k1)
= E &
dom H1(
l1)
= E )
by FUNCT_2:def 1;
A17:
H1(
k1 + 1)
. xx =
(H1(k1) * f) . xx
by FUNCT_7:71
.=
H1(
k1)
. (f . xx)
by A16, FUNCT_1:23
;
H1(
k1 + 1)
. xx =
(f * H1(k1)) . xx
by FUNCT_7:73
.=
f . (H1(k1) . xx)
by A16, FUNCT_1:23
.=
f . ((f * H1(k)) . xx)
by FUNCT_7:73
.=
f . (f . (H1(l) . x0))
by A15, A16, FUNCT_1:23
.=
f . ((f * H1(l)) . x0)
by A16, FUNCT_1:23
.=
f . (H1(l1) . x0)
by FUNCT_7:73
.=
(f * H1(l1)) . x0
by A16, FUNCT_1:23
.=
H1(
l2)
. x0
by FUNCT_7:73
;
then
yc in c2
by A13, A14, A17;
hence
y in c2
;
:: thesis: verum
end;
hence
f .: (b `1 ) misses b `1
by A4, A5, XBOOLE_1:63;
:: thesis: verum
end; thus
f .: (b `2 ) misses b `2
:: thesis: f .: (b `3 ) misses b `3 proof
f .: c2 c= c1
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in f .: c2 or y in c1 )
assume
y in f .: c2
;
:: thesis: y in c1
then consider x being
set such that A18:
(
x in dom f &
x in c2 &
y = f . x )
by FUNCT_1:def 12;
consider xx being
Element of
c such that A19:
(
x = xx & ex
k,
l being
Element of
NAT st
(
H1(
k)
. xx = H1(
l)
. x0 & not
k is
even &
l is
even ) )
by A18;
reconsider yc =
y as
Element of
c by A18, A19, Th6;
consider k,
l being
Element of
NAT such that A20:
(
H1(
k)
. xx = H1(
l)
. x0 & not
k is
even &
l is
even )
by A19;
reconsider k =
k as
odd Element of
NAT by A20;
reconsider l =
l as
even Element of
NAT by A20;
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 ;
A21:
(
dom f = E &
dom H1(
k)
= E &
dom H1(
l)
= E &
dom H1(
k1)
= E &
dom H1(
l1)
= E )
by FUNCT_2:def 1;
A22:
H1(
k1 + 1)
. xx =
(H1(k1) * f) . xx
by FUNCT_7:71
.=
H1(
k1)
. (f . xx)
by A21, FUNCT_1:23
;
H1(
k1 + 1)
. xx =
(f * H1(k1)) . xx
by FUNCT_7:73
.=
f . (H1(k1) . xx)
by A21, FUNCT_1:23
.=
f . ((f * H1(k)) . xx)
by FUNCT_7:73
.=
f . (f . (H1(l) . x0))
by A20, A21, FUNCT_1:23
.=
f . ((f * H1(l)) . x0)
by A21, FUNCT_1:23
.=
f . (H1(l1) . x0)
by FUNCT_7:73
.=
(f * H1(l1)) . x0
by A21, FUNCT_1:23
.=
H1(
l2)
. x0
by FUNCT_7:73
;
then
yc in c1
by A18, A19, A22;
hence
y in c1
;
:: thesis: verum
end;
hence
f .: (b `2 ) misses b `2
by A4, A5, XBOOLE_1:63;
:: thesis: verum
end; thus
f .: (b `3 ) misses b `3
by A5, XBOOLE_1:65;
:: 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
set such that A23:
(
x1 in c1 &
x1 in c2 )
by XBOOLE_0:3;
consider x11 being
Element of
c such that A24:
(
x1 = x11 & ex
k,
l being
Element of
NAT st
(
H1(
k)
. x11 = H1(
l)
. x0 &
k is
even &
l is
even ) )
by A23;
consider x12 being
Element of
c such that A25:
(
x1 = x12 & ex
k,
l being
Element of
NAT st
(
H1(
k)
. x12 = H1(
l)
. x0 & not
k is
even &
l is
even ) )
by A23;
reconsider x1 =
x1 as
Element of
c by A24;
consider k1,
l1 being
Element of
NAT such that A26:
(
H1(
k1)
. x11 = H1(
l1)
. x0 &
k1 is
even &
l1 is
even )
by A24;
consider k2,
l2 being
Element of
NAT such that A27:
(
H1(
k2)
. x12 = H1(
l2)
. x0 & not
k2 is
even &
l2 is
even )
by A25;
A28:
(
dom H1(
k1)
= E &
dom H1(
k2)
= E &
dom H1(
l1)
= E &
dom H1(
l2)
= E )
by FUNCT_2:def 1;
A29:
H1(
l1 + k2)
. x1 =
(H1(l1) * H1(k2)) . x1
by FUNCT_7:79
.=
H1(
l1)
. (H1(l2) . x0)
by A25, A27, A28, FUNCT_1:23
.=
(H1(l1) * H1(l2)) . x0
by A28, FUNCT_1:23
.=
H1(
l1 + l2)
. x0
by FUNCT_7:79
;
A30:
H1(
l2 + k1)
. x1 =
(H1(l2) * H1(k1)) . x1
by FUNCT_7:79
.=
H1(
l2)
. (H1(l1) . x0)
by A24, A26, A28, FUNCT_1:23
.=
(H1(l2) * H1(l1)) . x0
by A28, FUNCT_1:23
.=
H1(
l1 + l2)
. x0
by FUNCT_7:79
;
ex
r being
Element of
E ex
k being
odd Element of
NAT st
(
H1(
k)
. r = r &
r in c )
then consider r being
Element of
E,
k being
odd Element of
NAT such that A34:
(
H1(
k)
. r = r &
r in c )
;
reconsider r =
r as
Element of
c by A34;
deffunc H2(
set )
-> set =
{ l where l is Element of NAT : H1(l) . $1 = r } ;
A35:
for
x being
Element of
c holds
H2(
x)
in bool NAT
consider Odl being
Function of
c,
bool NAT such that A36:
for
x being
Element of
c holds
Odl . x = H2(
x)
from FUNCT_2:sch 8(A35);
now let n be
set ;
:: thesis: ( n in dom Odl implies not Odl . n is empty )assume
n in dom Odl
;
:: thesis: not Odl . n is emptythen reconsider nc =
n as
Element of
c by FUNCT_2:def 1;
A37:
Odl . nc = { l where l is Element of NAT : H1(l) . nc = r }
by A36;
consider x' being
set such that A38:
(
x' in E &
c = Class (=_ f),
x' )
by EQREL_1:def 5;
[nc,r] in =_ f
by A38, EQREL_1:30;
then consider kn,
ln being
Element of
NAT such that A39:
(iter f,kn) . nc = (iter f,ln) . r
by Def7;
defpred S4[
Element of
NAT ]
means H1(
k * $1)
. r = r;
A40:
S4[
0 ]
by Th3;
A44:
for
i being
Element of
NAT holds
S4[
i]
from NAT_1:sch 1(A40, A41);
A45:
2
* 0 <> k
;
set dk =
ln div k;
set mk =
ln mod k;
A46:
ln = (k * (ln div k)) + (ln mod k)
by A45, NAT_1:3, NAT_D:2;
ln mod k < k
by A45, NAT_1:3, NAT_D:1;
then reconsider kmk =
k - (ln mod k) as
Element of
NAT by INT_1:18;
A47:
ln + kmk = k * ((ln div k) + 1)
by A46;
A48:
(
dom H1(
kn)
= E &
dom H1(
ln)
= E )
by FUNCT_2:def 1;
H1(
kmk + kn)
. nc =
(H1(kmk) * H1(kn)) . nc
by FUNCT_7:79
.=
H1(
kmk)
. (H1(ln) . r)
by A39, A48, FUNCT_1:23
.=
(H1(kmk) * H1(ln)) . r
by A48, FUNCT_1:23
.=
H1(
k * ((ln div k) + 1))
. r
by A47, FUNCT_7:79
.=
r
by A44
;
then
kn + kmk in Odl . n
by A37;
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 15;
deffunc H3(
Element of
c)
-> Element of
NAT =
min (Odl . $1);
consider odl being
Function of
c,
NAT such that A49:
for
x being
Element of
c holds
odl . x = H3(
x)
from FUNCT_2:sch 4();
defpred S4[
set ]
means odl . $1 is
even;
defpred S5[
set ]
means not
odl . $1 is
even;
set c1 =
{ x where x is Element of c : S4[x] } ;
set d2 =
{ x where x is Element of c : S5[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
{ x where x is Element of c : S4[x] } \ {r} c= c
by XBOOLE_1:1;
then reconsider d1 =
{ x where x is Element of c : S4[x] } \ {r} as
Subset of
E by XBOOLE_1:1;
{ 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;
reconsider d3 =
{r} as
Subset of
E by ZFMISC_1:37;
take b =
[d1,d2,d3];
:: thesis: S1[c,b]A50:
(
b `1 = d1 &
b `2 = d2 &
b `3 = d3 )
by MCART_1:47;
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 A36;
then
min (Odl . r) = 0
by Th2;
then A51:
odl . r = 2
* 0
by A49;
then A52:
r in { x where x is Element of c : S4[x] }
;
A53:
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 A52, ZFMISC_1:46
;
{ x where x is Element of c : S4[x] } \/ d2 = c
hence
((b `1 ) \/ (b `2 )) \/ (b `3 ) = c
by A50, A53, XBOOLE_1:4;
:: thesis: ( f .: (b `1 ) misses b `1 & f .: (b `2 ) misses b `2 & f .: (b `3 ) misses b `3 )A57:
{ x where x is Element of c : S4[x] } misses d2
then A59:
d1 misses d2
by XBOOLE_1:63;
A60:
for
x being
Element of
c st
x <> r holds
odl . (f . x) = (odl . x) - 1
thus
f .: (b `1 ) misses b `1
:: thesis: ( f .: (b `2 ) misses b `2 & f .: (b `3 ) misses b `3 )thus
f .: (b `2 ) misses b `2
:: thesis: f .: (b `3 ) misses b `3 thus
f .: (b `3 ) misses b `3
:: thesis: verum end;
end;
consider F being Function of Class (=_ f),[:(bool E),(bool E),(bool E):] such that
A76:
for a being Element of Class (=_ f) holds S1[a,F . a]
from FUNCT_2:sch 3(A2);
set E1c = { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ;
set E1 = union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ;
set E2c = { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ;
set E2 = union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ;
set E3c = { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ;
set E3 = union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ;
take
union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum }
; :: thesis: ex E2, E3 being set st
( ((union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) \/ E2) \/ E3 = E & f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } & f .: E2 misses E2 & f .: E3 misses E3 )
take
union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum }
; :: thesis: ex E3 being set st
( ((union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )) \/ E3 = E & f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } & f .: E3 misses E3 )
take
union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum }
; :: thesis: ( ((union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) = E & f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )
thus
((union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) \/ (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )) \/ (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) = E
:: thesis: ( f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )
thus
f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum }
:: thesis: ( f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } & f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )proof
assume
not
f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum }
;
:: thesis: contradiction
then consider x being
set such that A90:
(
x in f .: (union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } ) &
x in union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } )
by XBOOLE_0:3;
consider Y being
set such that A91:
(
x in Y &
Y in { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } )
by A90, TARSKI:def 4;
consider c being
Element of
Class (=_ f) such that A92:
Y = (F . c) `1
by A91;
consider xx being
set such that A93:
(
xx in dom f &
xx in union { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } &
x = f . xx )
by A90, FUNCT_1:def 12;
consider YY being
set such that A94:
(
xx in YY &
YY in { ((F . c) `1 ) where c is Element of Class (=_ f) : verum } )
by A93, TARSKI:def 4;
consider cc being
Element of
Class (=_ f) such that A95:
YY = (F . cc) `1
by A94;
x in ((F . c) `1 ) \/ ((F . c) `2 )
by A91, A92, XBOOLE_0:def 3;
then
x in (((F . c) `1 ) \/ ((F . c) `2 )) \/ ((F . c) `3 )
by XBOOLE_0:def 3;
then A96:
x in c
by A76;
consider x' being
set such that A97:
(
x' in E &
c = Class (=_ f),
x' )
by EQREL_1:def 5;
A98:
c = Class (=_ f),
x
by A96, A97, EQREL_1:31;
xx in ((F . cc) `1 ) \/ ((F . cc) `2 )
by A94, A95, XBOOLE_0:def 3;
then
xx in (((F . cc) `1 ) \/ ((F . cc) `2 )) \/ ((F . cc) `3 )
by XBOOLE_0:def 3;
then A99:
xx in cc
by A76;
consider xx' being
set such that A100:
(
xx' in E &
cc = Class (=_ f),
xx' )
by EQREL_1:def 5;
A101:
cc = Class (=_ f),
xx
by A99, A100, EQREL_1:31;
dom f = E
by FUNCT_2:def 1;
then A102:
x in (dom f) \/ (rng f)
by A91, A92, XBOOLE_0:def 3;
(iter f,1) . xx =
x
by A93, FUNCT_7:72
.=
(id ((dom f) \/ (rng f))) . x
by A102, FUNCT_1:34
.=
(iter f,0 ) . x
by FUNCT_7:70
;
then
[x,xx] in =_ f
by A91, A92, A94, A95, Def7;
then A103:
Class (=_ f),
x = Class (=_ f),
xx
by A91, A92, EQREL_1:44;
A104:
f . xx in f .: YY
by A93, A94, FUNCT_1:def 12;
f .: YY misses YY
by A76, A95;
hence
contradiction
by A91, A92, A93, A95, A98, A101, A103, A104, XBOOLE_0:3;
:: thesis: verum
end;
thus
f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum }
:: thesis: f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } proof
assume
not
f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum }
;
:: thesis: contradiction
then consider x being
set such that A105:
(
x in f .: (union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } ) &
x in union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )
by XBOOLE_0:3;
consider Y being
set such that A106:
(
x in Y &
Y in { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )
by A105, TARSKI:def 4;
consider c being
Element of
Class (=_ f) such that A107:
Y = (F . c) `2
by A106;
consider xx being
set such that A108:
(
xx in dom f &
xx in union { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } &
x = f . xx )
by A105, FUNCT_1:def 12;
consider YY being
set such that A109:
(
xx in YY &
YY in { ((F . c) `2 ) where c is Element of Class (=_ f) : verum } )
by A108, TARSKI:def 4;
consider cc being
Element of
Class (=_ f) such that A110:
YY = (F . cc) `2
by A109;
x in ((F . c) `1 ) \/ ((F . c) `2 )
by A106, A107, XBOOLE_0:def 3;
then
x in (((F . c) `1 ) \/ ((F . c) `2 )) \/ ((F . c) `3 )
by XBOOLE_0:def 3;
then A111:
x in c
by A76;
consider x' being
set such that A112:
(
x' in E &
c = Class (=_ f),
x' )
by EQREL_1:def 5;
A113:
c = Class (=_ f),
x
by A111, A112, EQREL_1:31;
xx in ((F . cc) `1 ) \/ ((F . cc) `2 )
by A109, A110, XBOOLE_0:def 3;
then
xx in (((F . cc) `1 ) \/ ((F . cc) `2 )) \/ ((F . cc) `3 )
by XBOOLE_0:def 3;
then A114:
xx in cc
by A76;
consider xx' being
set such that A115:
(
xx' in E &
cc = Class (=_ f),
xx' )
by EQREL_1:def 5;
A116:
cc = Class (=_ f),
xx
by A114, A115, EQREL_1:31;
dom f = E
by FUNCT_2:def 1;
then A117:
x in (dom f) \/ (rng f)
by A106, A107, XBOOLE_0:def 3;
(iter f,1) . xx =
x
by A108, FUNCT_7:72
.=
(id ((dom f) \/ (rng f))) . x
by A117, FUNCT_1:34
.=
(iter f,0 ) . x
by FUNCT_7:70
;
then
[x,xx] in =_ f
by A106, A107, A109, A110, Def7;
then A118:
Class (=_ f),
x = Class (=_ f),
xx
by A106, A107, EQREL_1:44;
A119:
f . xx in f .: YY
by A108, A109, FUNCT_1:def 12;
f .: YY misses YY
by A76, A110;
hence
contradiction
by A106, A107, A108, A110, A113, A116, A118, A119, XBOOLE_0:3;
:: thesis: verum
end;
thus
f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum }
:: thesis: verumproof
assume
not
f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) misses union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum }
;
:: thesis: contradiction
then consider x being
set such that A120:
(
x in f .: (union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } ) &
x in union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )
by XBOOLE_0:3;
consider Y being
set such that A121:
(
x in Y &
Y in { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )
by A120, TARSKI:def 4;
consider c being
Element of
Class (=_ f) such that A122:
Y = (F . c) `3
by A121;
consider xx being
set such that A123:
(
xx in dom f &
xx in union { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } &
x = f . xx )
by A120, FUNCT_1:def 12;
consider YY being
set such that A124:
(
xx in YY &
YY in { ((F . c) `3 ) where c is Element of Class (=_ f) : verum } )
by A123, TARSKI:def 4;
consider cc being
Element of
Class (=_ f) such that A125:
YY = (F . cc) `3
by A124;
x in (((F . c) `1 ) \/ ((F . c) `2 )) \/ ((F . c) `3 )
by A121, A122, XBOOLE_0:def 3;
then A126:
x in c
by A76;
consider x' being
set such that A127:
(
x' in E &
c = Class (=_ f),
x' )
by EQREL_1:def 5;
A128:
c = Class (=_ f),
x
by A126, A127, EQREL_1:31;
xx in (((F . cc) `1 ) \/ ((F . cc) `2 )) \/ ((F . cc) `3 )
by A124, A125, XBOOLE_0:def 3;
then A129:
xx in cc
by A76;
consider xx' being
set such that A130:
(
xx' in E &
cc = Class (=_ f),
xx' )
by EQREL_1:def 5;
A131:
cc = Class (=_ f),
xx
by A129, A130, EQREL_1:31;
dom f = E
by FUNCT_2:def 1;
then A132:
x in (dom f) \/ (rng f)
by A121, A122, XBOOLE_0:def 3;
(iter f,1) . xx =
x
by A123, FUNCT_7:72
.=
(id ((dom f) \/ (rng f))) . x
by A132, FUNCT_1:34
.=
(iter f,0 ) . x
by FUNCT_7:70
;
then
[x,xx] in =_ f
by A121, A122, A124, A125, Def7;
then A133:
Class (=_ f),
x = Class (=_ f),
xx
by A121, A122, EQREL_1:44;
A134:
f . xx in f .: YY
by A123, A124, FUNCT_1:def 12;
f .: YY misses YY
by A76, A125;
hence
contradiction
by A121, A122, A123, A125, A128, A131, A133, A134, XBOOLE_0:3;
:: thesis: verum
end;