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;
let x be object ; TARSKI:def 3 ( not x in Vars or x in Rank omega )
assume
x in Vars
; x in Rank omega
then consider i being object such that
A4:
i in dom V
and
A5:
x in V . i
by A1, CARD_5:2;
reconsider i = i as Element of NAT by A4;
defpred S1[ Nat] means V . $1 c= Rank omega;
A6:
S1[ 0 ]
proof
let x be
object ;
TARSKI:def 3 ( not x in V . 0 or x in Rank omega )
assume
x in V . 0
;
x in Rank omega
then consider i being
Element of
NAT such that A7:
x = [{},i]
by A2;
A8:
Segm (i + 1) = succ (Segm i)
by NAT_1:38;
A9:
{} c= i
;
A10:
i in i + 1
by A8, ORDINAL1:6;
A11:
{} in i + 1
by A8, A9, ORDINAL1:6, ORDINAL1:12;
A12:
the_rank_of {} = {}
by CLASSES1:73;
A13:
the_rank_of i = i
by CLASSES1:73;
A14:
{} in Rank (i + 1)
by A11, A12, CLASSES1:66;
i in Rank (i + 1)
by A10, A13, CLASSES1:66;
then A15:
x in Rank (succ (succ (i + 1)))
by A7, A14, CLASSES1:45;
succ (succ (i + 1)) c= omega
;
then
Rank (succ (succ (i + 1))) c= Rank omega
by CLASSES1:37;
hence
x in Rank omega
by A15;
verum
end;
A16:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A17:
S1[
n]
;
S1[n + 1]A18:
V . (n + 1) = { [(varcl a),j] where a is Subset of (V . n), j is Element of NAT : a is finite }
by A3;
thus
S1[
n + 1]
verumproof
let x be
object ;
TARSKI:def 3 ( not x in V . (n + 1) or x in Rank omega )
assume
x in V . (n + 1)
;
x in Rank omega
then consider a being
Subset of
(V . n),
j being
Element of
NAT such that A19:
x = [(varcl a),j]
and A20:
a is
finite
by A18;
a c= Rank omega
by A17, XBOOLE_1:1;
then
a in Rank omega
by A20, Th22;
then reconsider i =
the_rank_of a as
Element of
NAT by CLASSES1:66;
reconsider k =
j \/ i as
Element of
NAT by ORDINAL3:12;
A21:
the_rank_of (varcl a) = i
by Th21;
A22:
the_rank_of j = j
by CLASSES1:73;
A23:
k in succ k
by ORDINAL1:6;
then A24:
i in succ k
by ORDINAL1:12, XBOOLE_1:7;
A25:
j in succ k
by A23, ORDINAL1:12, XBOOLE_1:7;
A26:
succ (Segm k) = Segm (k + 1)
by NAT_1:38;
then A27:
varcl a in Rank (k + 1)
by A21, A24, CLASSES1:66;
j in Rank (k + 1)
by A22, A25, A26, CLASSES1:66;
then A28:
x in Rank (succ (succ (k + 1)))
by A19, A27, CLASSES1:45;
succ (succ (k + 1)) c= omega
;
then
Rank (succ (succ (k + 1))) c= Rank omega
by CLASSES1:37;
hence
x in Rank omega
by A28;
verum
end; end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A16);
then
V . i c= Rank omega
;
hence
x in Rank omega
by A5; verum