let V be ManySortedSet of NAT ; ( 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 i, j being Element of NAT st i <= j holds
V . i c= V . j )
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 }
; for i, j being Element of NAT st i <= j holds
V . i c= V . j
defpred S1[ Nat] means V . 0 c= V . $1;
defpred S2[ Nat] means for i being Nat st i <= $1 holds
V . i c= V . $1;
A6:
S2[ 0 ]
by NAT_1:3;
A7:
now for j being Nat st S2[j] holds
S2[j + 1]let j be
Nat;
( S2[j] implies S2[j + 1] )assume A8:
S2[
j]
;
S2[j + 1]A9:
V . j c= V . (j + 1)
proof
per cases
( j = 0 or ex k being Nat st j = k + 1 )
by NAT_1:6;
suppose
ex
k being
Nat st
j = k + 1
;
V . j c= V . (j + 1)then consider k being
Nat such that A10:
j = k + 1
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A11:
V . j = { [(varcl A),n] where A is Subset of (V . k), n is Element of NAT : A is finite }
by A2, A10;
A12:
V . (j + 1) = { [(varcl A),n] where A is Subset of (V . j), n is Element of NAT : A is finite }
by A2;
A13:
V . k c= V . j
by A8, A10, NAT_1:11;
let x be
object ;
TARSKI:def 3 ( not x in V . j or x in V . (j + 1) )assume
x in V . j
;
x in V . (j + 1)then consider A being
Subset of
(V . k),
n being
Element of
NAT such that A14:
x = [(varcl A),n]
and A15:
A is
finite
by A11;
A c= V . j
by A13;
hence
x in V . (j + 1)
by A12, A14, A15;
verum end; end;
end; thus
S2[
j + 1]
verum end;
for j being Nat holds S2[j]
from NAT_1:sch 2(A6, A7);
hence
for i, j being Element of NAT st i <= j holds
V . i c= V . j
; verum