consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V . 0 = { [{},i] where i is Element of NAT : verum } and
A3: 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 } by Def2;
set X = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } ;
A4: dom V = NAT by PARTFUN1:def 2;
defpred S1[ Nat] means V . $1 c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } ;
A5: S1[ 0 ]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V . 0 or x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } )
assume A6: x in V . 0 ; :: thesis: x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }
A7: {} c= Vars ;
ex i being Element of NAT st x = [{},i] by A2, A6;
hence x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } by A7, Th8; :: thesis: verum
end;
A8: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; :: thesis: S1[i + 1]
A9: V . (i + 1) = { [(varcl A),j] where A is Subset of (V . i), j is Element of NAT : A is finite } by A3;
thus S1[i + 1] :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V . (i + 1) or x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } )
assume x in V . (i + 1) ; :: thesis: x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }
then consider A being Subset of (V . i), j being Element of NAT such that
A10: x = [(varcl A),j] and
A11: A is finite by A9;
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
V . ii in rng V by A4, FUNCT_1:def 3;
then V . i c= Vars by A1, ZFMISC_1:74;
then A c= Vars ;
hence x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } by A10, A11; :: thesis: verum
end;
end;
A12: for i being Nat holds S1[i] from NAT_1:sch 2(A5, A8);
now :: thesis: for x being set st x in rng V holds
x c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }
let x be set ; :: thesis: ( x in rng V implies x c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } )
assume x in rng V ; :: thesis: x c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }
then ex y being object st
( y in NAT & x = V . y ) by A4, FUNCT_1:def 3;
hence x c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } by A12; :: thesis: verum
end;
hence Vars c= { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } by A1, ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis: { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } c= Vars
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } or x in Vars )
assume x in { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } ; :: thesis: x in Vars
then ex A being Subset of Vars ex j being Element of NAT st
( x = [(varcl A),j] & A is finite ) ;
hence x in Vars by Th17; :: thesis: verum