let A be non empty finite Subset of NAT; :: thesis: ( union A in A & ( for a being set holds

( not a in A or a in union A or a = union A ) ) )

consider a being Ordinal such that

A1: RelIncl A, RelIncl a are_isomorphic by WELLORD2:8, WELLORD2:13;

consider F1 being Function such that

A2: F1 is_isomorphism_of RelIncl A, RelIncl a by A1, WELLORD1:def 8;

A3: dom F1 = field (RelIncl A) by A2, WELLORD1:def 7;

then dom F1 = A by WELLORD2:def 1;

then consider b being object such that

A4: b in dom F1 by XBOOLE_0:def 1;

rng F1 is finite by A3, FINSET_1:8;

then field (RelIncl a) is finite by A2, WELLORD1:def 7;

then A5: a is finite by WELLORD2:def 1;

F1 . b in rng F1 by A4, FUNCT_1:3;

then not field (RelIncl a) is empty by A2, WELLORD1:def 7;

then not a is empty by WELLORD2:def 1;

then A6: {} in a by ORDINAL1:16, XBOOLE_1:3;

then consider F being Function such that

A8: F is_isomorphism_of RelIncl a, RelIncl A by WELLORD1:def 8;

A9: for m, n being Nat st m in dom F & n in dom F & n < m holds

F . n in F . m

dom F = field (RelIncl a) by A8, WELLORD1:def 7;

then A18: dom F = a by WELLORD2:def 1;

A23: succ m = a ;

A24: rng F = field (RelIncl A) by A8, WELLORD1:def 7;

then A25: rng F = A by WELLORD2:def 1;

then reconsider F = F as Function of a,A by A18, FUNCT_2:1;

A26: for n, m being Nat st m in dom F & n in dom F & n < m holds

F . n in F . m by A9;

rng F = A by A24, WELLORD2:def 1;

then A27: F . (union a) = union (rng F) by A21, A26, Th1;

A28: union a = m by A23, ORDINAL2:2;

hence union A in A by A25, A18, A23, A27, FUNCT_1:3, ORDINAL1:6; :: thesis: for a being set holds

( not a in A or a in union A or a = union A )

thus for b being set holds

( not b in A or b in union A or b = union A ) :: thesis: verum

( not a in A or a in union A or a = union A ) ) )

consider a being Ordinal such that

A1: RelIncl A, RelIncl a are_isomorphic by WELLORD2:8, WELLORD2:13;

consider F1 being Function such that

A2: F1 is_isomorphism_of RelIncl A, RelIncl a by A1, WELLORD1:def 8;

A3: dom F1 = field (RelIncl A) by A2, WELLORD1:def 7;

then dom F1 = A by WELLORD2:def 1;

then consider b being object such that

A4: b in dom F1 by XBOOLE_0:def 1;

rng F1 is finite by A3, FINSET_1:8;

then field (RelIncl a) is finite by A2, WELLORD1:def 7;

then A5: a is finite by WELLORD2:def 1;

F1 . b in rng F1 by A4, FUNCT_1:3;

then not field (RelIncl a) is empty by A2, WELLORD1:def 7;

then not a is empty by WELLORD2:def 1;

then A6: {} in a by ORDINAL1:16, XBOOLE_1:3;

A7: now :: thesis: not a is limit_ordinal

RelIncl a, RelIncl A are_isomorphic
by A1, WELLORD1:40;assume
a is limit_ordinal
; :: thesis: contradiction

then omega c= a by A6, ORDINAL1:def 11;

hence contradiction by A5; :: thesis: verum

end;then omega c= a by A6, ORDINAL1:def 11;

hence contradiction by A5; :: thesis: verum

then consider F being Function such that

A8: F is_isomorphism_of RelIncl a, RelIncl A by WELLORD1:def 8;

A9: for m, n being Nat st m in dom F & n in dom F & n < m holds

F . n in F . m

proof

reconsider a = a as Nat by A5;
let m, n be Nat; :: thesis: ( m in dom F & n in dom F & n < m implies F . n in F . m )

assume that

A10: m in dom F and

A11: n in dom F and

A12: n < m ; :: thesis: F . n in F . m

F . n in rng F by A11, FUNCT_1:3;

then F . n in field (RelIncl A) by A8, WELLORD1:def 7;

then A13: F . n in A by WELLORD2:def 1;

then reconsider b = F . n as Nat ;

n in field (RelIncl a) by A8, A11, WELLORD1:def 7;

then A14: n in a by WELLORD2:def 1;

F . m in rng F by A10, FUNCT_1:3;

then F . m in field (RelIncl A) by A8, WELLORD1:def 7;

then A15: F . m in A by WELLORD2:def 1;

then reconsider c = F . m as Nat ;

n in { i where i is Nat : i < m } by A12;

then n in m by AXIOMS:4;

then A16: n c= m by ORDINAL1:def 2;

m in field (RelIncl a) by A8, A10, WELLORD1:def 7;

then m in a by WELLORD2:def 1;

then [n,m] in RelIncl a by A14, A16, WELLORD2:def 1;

then [(F . n),(F . m)] in RelIncl A by A8, WELLORD1:def 7;

then A17: F . n c= F . m by A13, A15, WELLORD2:def 1;

F is one-to-one by A8, WELLORD1:def 7;

then F . n <> F . m by A10, A11, A12;

then F . n c< F . m by A17;

then b in c by ORDINAL1:11;

hence F . n in F . m ; :: thesis: verum

end;assume that

A10: m in dom F and

A11: n in dom F and

A12: n < m ; :: thesis: F . n in F . m

F . n in rng F by A11, FUNCT_1:3;

then F . n in field (RelIncl A) by A8, WELLORD1:def 7;

then A13: F . n in A by WELLORD2:def 1;

then reconsider b = F . n as Nat ;

n in field (RelIncl a) by A8, A11, WELLORD1:def 7;

then A14: n in a by WELLORD2:def 1;

F . m in rng F by A10, FUNCT_1:3;

then F . m in field (RelIncl A) by A8, WELLORD1:def 7;

then A15: F . m in A by WELLORD2:def 1;

then reconsider c = F . m as Nat ;

n in { i where i is Nat : i < m } by A12;

then n in m by AXIOMS:4;

then A16: n c= m by ORDINAL1:def 2;

m in field (RelIncl a) by A8, A10, WELLORD1:def 7;

then m in a by WELLORD2:def 1;

then [n,m] in RelIncl a by A14, A16, WELLORD2:def 1;

then [(F . n),(F . m)] in RelIncl A by A8, WELLORD1:def 7;

then A17: F . n c= F . m by A13, A15, WELLORD2:def 1;

F is one-to-one by A8, WELLORD1:def 7;

then F . n <> F . m by A10, A11, A12;

then F . n c< F . m by A17;

then b in c by ORDINAL1:11;

hence F . n in F . m ; :: thesis: verum

dom F = field (RelIncl a) by A8, WELLORD1:def 7;

then A18: dom F = a by WELLORD2:def 1;

A19: now :: thesis: for b being Ordinal st succ b = a holds

b in NAT

A21:
ex m being Nat st succ m = a
b in NAT

let b be Ordinal; :: thesis: ( succ b = a implies b in NAT )

A20: a in NAT by ORDINAL1:def 12;

assume succ b = a ; :: thesis: b in NAT

then b in a by ORDINAL1:6;

hence b in NAT by ORDINAL1:10, A20; :: thesis: verum

end;A20: a in NAT by ORDINAL1:def 12;

assume succ b = a ; :: thesis: b in NAT

then b in a by ORDINAL1:6;

hence b in NAT by ORDINAL1:10, A20; :: thesis: verum

proof

then consider m being Nat such that
consider b being Ordinal such that

A22: succ b = a by A7, ORDINAL1:29;

reconsider b = b as Element of NAT by A19, A22;

take b ; :: thesis: succ b = a

thus succ b = a by A22; :: thesis: verum

end;A22: succ b = a by A7, ORDINAL1:29;

reconsider b = b as Element of NAT by A19, A22;

take b ; :: thesis: succ b = a

thus succ b = a by A22; :: thesis: verum

A23: succ m = a ;

A24: rng F = field (RelIncl A) by A8, WELLORD1:def 7;

then A25: rng F = A by WELLORD2:def 1;

then reconsider F = F as Function of a,A by A18, FUNCT_2:1;

A26: for n, m being Nat st m in dom F & n in dom F & n < m holds

F . n in F . m by A9;

rng F = A by A24, WELLORD2:def 1;

then A27: F . (union a) = union (rng F) by A21, A26, Th1;

A28: union a = m by A23, ORDINAL2:2;

hence union A in A by A25, A18, A23, A27, FUNCT_1:3, ORDINAL1:6; :: thesis: for a being set holds

( not a in A or a in union A or a = union A )

thus for b being set holds

( not b in A or b in union A or b = union A ) :: thesis: verum

proof

let b be set ; :: thesis: ( not b in A or b in union A or b = union A )

assume A29: b in A ; :: thesis: ( b in union A or b = union A )

end;assume A29: b in A ; :: thesis: ( b in union A or b = union A )

now :: thesis: ( not b <> union A or b in union A or b = union A )

hence
( b in union A or b = union A )
; :: thesis: verumA30:
m in dom F
by A18, A23, ORDINAL1:6;

assume A31: b <> union A ; :: thesis: ( b in union A or b = union A )

consider c being object such that

A32: c in dom F and

A33: F . c = b by A25, A29, FUNCT_1:def 3;

dom F = a by PARTFUN1:def 2;

then A34: dom F in NAT by ORDINAL1:def 12;

reconsider c = c as Element of NAT by A32, ORDINAL1:10, A34;

( c in m or c = m ) by A23, A32, ORDINAL1:8;

then c in { k where k is Nat : k < m } by A25, A23, A27, A31, A33, AXIOMS:4, ORDINAL2:2;

then ex k being Nat st

( k = c & k < m ) ;

hence ( b in union A or b = union A ) by A9, A25, A27, A28, A32, A33, A30; :: thesis: verum

end;assume A31: b <> union A ; :: thesis: ( b in union A or b = union A )

consider c being object such that

A32: c in dom F and

A33: F . c = b by A25, A29, FUNCT_1:def 3;

dom F = a by PARTFUN1:def 2;

then A34: dom F in NAT by ORDINAL1:def 12;

reconsider c = c as Element of NAT by A32, ORDINAL1:10, A34;

( c in m or c = m ) by A23, A32, ORDINAL1:8;

then c in { k where k is Nat : k < m } by A25, A23, A27, A31, A33, AXIOMS:4, ORDINAL2:2;

then ex k being Nat st

( k = c & k < m ) ;

hence ( b in union A or b = union A ) by A9, A25, A27, A28, A32, A33, A30; :: thesis: verum