let V be ManySortedSet of NAT ; :: thesis: ( V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) implies for A being finite Subset of Vars ex i being Element of NAT st A c= V . i )
assume that
A1: V . 0 = { [{},i] where i is Element of NAT : verum } and
A2: for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ; :: thesis: for A being finite Subset of Vars ex i being Element of NAT st A c= V . i
let A be finite Subset of Vars; :: thesis: ex i being Element of NAT st A c= V . i
A3: Vars = Union V by A1, A2, Def2;
defpred S1[ object , object ] means $1 in V . $2;
A4: now :: thesis: for x being object st x in A holds
ex i being object st
( i in NAT & S1[x,i] )
let x be object ; :: thesis: ( x in A implies ex i being object st
( i in NAT & S1[x,i] ) )
assume x in A ; :: thesis: ex i being object st
( i in NAT & S1[x,i] )
then consider Y being set such that
A5: x in Y and
A6: Y in rng V by A3, TARSKI:def 4;
consider i being object such that
A7: i in dom V and
A8: Y = V . i by A6, FUNCT_1:def 3;
reconsider i = i as object ;
take i = i; :: thesis: ( i in NAT & S1[x,i] )
thus ( i in NAT & S1[x,i] ) by A5, A7, A8; :: thesis: verum
end;
consider f being Function such that
A9: ( dom f = A & rng f c= NAT ) and
A10: for x being object st x in A holds
S1[x,f . x] from FUNCT_1:sch 6(A4);
per cases ( A = {} or A <> {} ) ;
suppose A = {} ; :: thesis: ex i being Element of NAT st A c= V . i
then A c= V . 0 ;
hence ex i being Element of NAT st A c= V . i ; :: thesis: verum
end;
suppose A <> {} ; :: thesis: ex i being Element of NAT st A c= V . i
then reconsider B = rng f as non empty finite Subset of NAT by A9, FINSET_1:8, RELAT_1:42;
reconsider i = max B as Element of NAT by ORDINAL1:def 12;
take i ; :: thesis: A c= V . i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in V . i )
assume A11: x in A ; :: thesis: x in V . i
then A12: f . x in B by A9, FUNCT_1:def 3;
then reconsider j = f . x as Element of NAT ;
j <= i by A12, XXREAL_2:def 8;
then A13: V . j c= V . i by A1, A2, Th14;
x in V . j by A10, A11;
hence x in V . i by A13; :: thesis: verum
end;
end;