defpred S1[ Element of F1(), Element of Fin F1()] means ex y being Element of F1() st
( y in $2 & P1[y,$1] & ( for z being Element of F1() st z in $2 & P1[z,y] holds
P1[y,z] ) );
defpred S2[ Element of Fin F1()] means for x being Element of F1() st x in $1 holds
S1[x,$1];
A3:
now for B being Element of Fin F1()
for x being Element of F1() st S2[B] holds
S2[B \/ {.x.}]let B be
Element of
Fin F1();
for x being Element of F1() st S2[B] holds
S2[B \/ {.x.}]let x be
Element of
F1();
( S2[B] implies S2[B \/ {.x.}] )assume A4:
S2[
B]
;
S2[B \/ {.x.}]thus
S2[
B \/ {.x.}]
verumproof
let z be
Element of
F1();
( z in B \/ {.x.} implies S1[z,B \/ {.x.}] )
assume A5:
z in B \/ {x}
;
S1[z,B \/ {.x.}]
now S1[z,B \/ {.x.}]per cases
( z in B or z = x )
by A5, ZFMISC_1:136;
suppose
z in B
;
S1[z,B \/ {.x.}]then consider y being
Element of
F1()
such that A6:
y in B
and A7:
P1[
y,
z]
and A8:
for
x being
Element of
F1() st
x in B &
P1[
x,
y] holds
P1[
y,
x]
by A4;
now ( ( P1[x,y] & x in B \/ {x} & P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) ) or ( P1[x,y] & y in B \/ {x} & P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) ) )per cases
( P1[x,y] or not P1[x,y] )
;
case A9:
P1[
x,
y]
;
( x in B \/ {x} & P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )thus
x in B \/ {x}
by ZFMISC_1:136;
( P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )thus
P1[
x,
z]
by A2, A7, A9;
for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]let v be
Element of
F1();
( v in B \/ {x} & P1[v,x] implies P1[x,v] )assume that A10:
v in B \/ {x}
and A11:
P1[
v,
x]
;
P1[x,v]A12:
now ( v in B implies P1[x,v] )assume A13:
v in B
;
P1[x,v]
P1[
v,
y]
by A2, A9, A11;
then
P1[
y,
v]
by A8, A13;
hence
P1[
x,
v]
by A2, A9;
verum end;
(
v in B or
v = x )
by A10, ZFMISC_1:136;
hence
P1[
x,
v]
by A1, A12;
verum end; case A14:
P1[
x,
y]
;
( y in B \/ {x} & P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )thus
y in B \/ {x}
by A6, XBOOLE_0:def 3;
( P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )thus
P1[
y,
z]
by A7;
for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v]let v be
Element of
F1();
( v in B \/ {x} & P1[v,y] implies P1[y,v] )assume that A15:
v in B \/ {x}
and A16:
P1[
v,
y]
;
P1[y,v]
(
v in B or
v = x )
by A15, ZFMISC_1:136;
hence
P1[
y,
v]
by A8, A14, A16;
verum end; end; end; hence
S1[
z,
B \/ {.x.}]
;
verum end; suppose A17:
z = x
;
S1[z,B \/ {.x.}]now ( ( ex w being Element of F1() st
( w in B & P1[w,x] ) & ex u being Element of F1() st
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) ) ) or ( ( for w being Element of F1() st w in B holds
not P1[w,x] ) & x in B \/ {x} & P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) ) )per cases
( ex w being Element of F1() st
( w in B & P1[w,x] ) or for w being Element of F1() st w in B holds
not P1[w,x] )
;
case
ex
w being
Element of
F1() st
(
w in B &
P1[
w,
x] )
;
ex u being Element of F1() st
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )then consider w being
Element of
F1()
such that A18:
w in B
and A19:
P1[
w,
z]
by A17;
consider y being
Element of
F1()
such that A20:
y in B
and A21:
P1[
y,
w]
and A22:
for
x being
Element of
F1() st
x in B &
P1[
x,
y] holds
P1[
y,
x]
by A4, A18;
take u =
y;
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )thus
u in B \/ {x}
by A20, XBOOLE_0:def 3;
( P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )thus
P1[
u,
z]
by A2, A19, A21;
for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v]let v be
Element of
F1();
( v in B \/ {x} & P1[v,u] implies P1[u,v] )assume that A23:
v in B \/ {x}
and A24:
P1[
v,
u]
;
P1[u,v]
(
v in B or
v = x )
by A23, ZFMISC_1:136;
hence
P1[
u,
v]
by A2, A17, A19, A21, A22, A24;
verum end; case A25:
for
w being
Element of
F1() st
w in B holds
not
P1[
w,
x]
;
( x in B \/ {x} & P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )thus
x in B \/ {x}
by ZFMISC_1:136;
( P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )thus A26:
P1[
x,
x]
by A1;
for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]let v be
Element of
F1();
( v in B \/ {x} & P1[v,x] implies P1[x,v] )assume that A27:
v in B \/ {x}
and A28:
P1[
v,
x]
;
P1[x,v]
not
v in B
by A25, A28;
hence
P1[
x,
v]
by A26, A27, ZFMISC_1:136;
verum end; end; end; hence
S1[
z,
B \/ {.x.}]
by A17;
verum end; end; end;
hence
S1[
z,
B \/ {.x.}]
;
verum
end; end;
A29:
S2[ {}. F1()]
;
for B being Element of Fin F1() holds S2[B]
from SETWISEO:sch 4(A29, A3);
hence
for x being Element of F1() st x in F2() holds
ex y being Element of F1() st
( y in F2() & P1[y,x] & ( for z being Element of F1() st z in F2() & P1[z,y] holds
P1[y,z] ) )
; verum