let A be non empty finite Subset of NAT; ( 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;
RelIncl a, RelIncl A are_isomorphic
by A1, WELLORD1:40;
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
let m,
n be
Nat;
( 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
;
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
;
verum
end;
reconsider a = a as Nat by A5;
dom F = field (RelIncl a)
by A8, WELLORD1:def 7;
then A18:
dom F = a
by WELLORD2:def 1;
A21:
ex m being Nat st succ m = a
then consider m being Nat such that
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; 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 )
verumproof
let b be
set ;
( not b in A or b in union A or b = union A )
assume A29:
b in A
;
( b in union A or b = union A )
now ( not b <> union A or b in union A or b = union A )A30:
m in dom F
by A18, A23, ORDINAL1:6;
assume A31:
b <> union A
;
( 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;
verum end;
hence
(
b in union A or
b = union A )
;
verum
end;