let V be Universe; :: thesis: for a being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let a be Element of V; :: thesis: for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let X be Subclass of V; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
let fs be finite Subset of omega; :: thesis: ( X is closed_wrt_A1-A7 & a in X implies Funcs (fs,a) in X )
defpred S₁[ set ] means Funcs ($1,a) in X;
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X ; :: thesis: Funcs (fs,a) in X
A3: X is closed_wrt_A4 by A1;
A4: X is closed_wrt_A5 by A1;
A5: for o, B being set st o in fs & B c= fs & S₁[B] holds
S₁[B \/ {o}]

proof

let o, B be set ; :: thesis: ( o in fs & B c= fs & S₁[B] implies S₁[B \/ {o}] )
assume that
A6: o in fs and
B c= fs and
A7: Funcs (B,a) in X ; :: thesis: S₁[B \/ {o}]

per cases ( B meets {o} or B misses {o} ) ;

suppose B meets {o} ; :: thesis: S₁[B \/ {o}]

hence S₁[B \/ {o}] by A7, ZFMISC_1:40, ZFMISC_1:50; :: thesis: verum

end;

suppose A8: B misses {o} ; :: thesis: S₁[B \/ {o}]

set r = {o};
set A = { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ;
A9: ( omega c= X & o in omega ) by A1, A6, Th7;
then o in X ;
then reconsider p = o as Element of V ;
A10: Funcs ({o},a) = { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }

proof

thus Funcs ({o},a) c= { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } :: according to XBOOLE_0:def 10 :: thesis: { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } c= Funcs ({o},a)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Funcs ({o},a) or q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } )
assume q in Funcs ({o},a) ; :: thesis: q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
then consider g being Function such that
A11: q = g and
A12: dom g = {o} and
A13: rng g c= a by FUNCT_2:def 2;
o in dom g by A12, TARSKI:def 1;
then A14: g . o in rng g by FUNCT_1:def 3;
then reconsider s = g . o as Element of V by A2, A13, Th1;
( o in {o} & g = {[p,s]} ) by A12, GRFUNC_1:7, TARSKI:def 1;
hence q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } by A11, A13, A14; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } or q in Funcs ({o},a) )
assume q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ; :: thesis: q in Funcs ({o},a)
then consider x, y being Element of V such that
A15: q = {[x,y]} and
A16: x in {o} and
A17: y in a ;
reconsider g = q as Function by A15;
rng g = {y} by A15, RELAT_1:9;
then A18: rng g c= a by A17, ZFMISC_1:31;
x = o by A16, TARSKI:def 1;
then dom g = {o} by A15, RELAT_1:9;
hence q in Funcs ({o},a) by A18, FUNCT_2:def 2; :: thesis: verum

end;

reconsider x = Funcs (B,a) as Element of V by A7;
{o} in X by A1, A9, Th2;
then A19: Funcs ({o},a) in X by A2, A3, A10;
then reconsider y = Funcs ({o},a) as Element of V ;
set Z = { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ;
Funcs ((B \/ {o}),a) = { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }

proof

thus Funcs ((B \/ {o}),a) c= { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } :: according to XBOOLE_0:def 10 :: thesis: { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } c= Funcs ((B \/ {o}),a)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Funcs ((B \/ {o}),a) or q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } )
assume q in Funcs ((B \/ {o}),a) ; :: thesis: q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) }
then consider g being Function such that
A20: q = g and
A21: dom g = B \/ {o} and
A22: rng g c= a by FUNCT_2:def 2;
set A = g | B;
rng (g | B) c= rng g by RELAT_1:70;
then A23: rng (g | B) c= a by A22;
set C = g | {o};
rng (g | {o}) c= rng g by RELAT_1:70;
then A24: rng (g | {o}) c= a by A22;
dom (g | {o}) = (B \/ {o}) /\ {o} by A21, RELAT_1:61
.= {o} by XBOOLE_1:21 ;
then A25: g | {o} in y by A24, FUNCT_2:def 2;
then reconsider y9 = g | {o} as Element of V by A19, Th1;
dom (g | B) = (B \/ {o}) /\ B by A21, RELAT_1:61
.= B by XBOOLE_1:21 ;
then A26: g | B in x by A23, FUNCT_2:def 2;
then reconsider x9 = g | B as Element of V by A7, Th1;
g = g | (B \/ {o}) by A21
.= (g | B) \/ (g | {o}) by RELAT_1:78 ;
then q = x9 \/ y9 by A20;
hence q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } by A26, A25; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } or q in Funcs ((B \/ {o}),a) )
assume q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ; :: thesis: q in Funcs ((B \/ {o}),a)
then consider x9, y9 being Element of V such that
A27: q = x9 \/ y9 and
A28: x9 in x and
A29: y9 in y ;
consider e being Function such that
A30: x9 = e and
A31: dom e = B and
A32: rng e c= a by A28, FUNCT_2:def 2;
consider g being Function such that
A33: y9 = g and
A34: dom g = {o} and
A35: rng g c= a by A29, FUNCT_2:def 2;
reconsider h = e \/ g as Function by A8, A31, A34, GRFUNC_1:13;
rng h = (rng e) \/ (rng g) by RELAT_1:12;
then A36: rng h c= a \/ a by A32, A35, XBOOLE_1:13;
dom h = B \/ {o} by A31, A34, XTUPLE_0:23;
hence q in Funcs ((B \/ {o}),a) by A27, A30, A33, A36, FUNCT_2:def 2; :: thesis: verum

end;

hence S₁[B \/ {o}] by A4, A7, A19; :: thesis: verum

end;

end;

end;

( Funcs ({},a) = {{}} & {} in X ) by A1, Th3, FUNCT_5:57;
then A37: S₁[ {} ] by A1, Th2;
A38: fs is finite ;
thus S₁[fs] from FINSET_1:sch 2(A38, A37, A5); :: thesis: verum