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 ]
A8:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume
S1[
i]
;
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]
verumproof
let x be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end; end;
A12:
for i being Nat holds S1[i]
from NAT_1:sch 2(A5, A8);
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; XBOOLE_0:def 10 { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } c= Vars
let x be object ; TARSKI:def 3 ( 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 }
; 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; verum