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:9, WELLORD2:14;
consider F1 being Function such that
A2:
F1 is_isomorphism_of RelIncl A, RelIncl a
by A1, WELLORD1:def 8;
dom F1 = field (RelIncl A)
by A2, WELLORD1:def 7;
then A3:
dom F1 = A
by WELLORD2:def 1;
then consider b being set such that
A4:
b in dom F1
by XBOOLE_0:def 1;
rng F1 is finite
by A3, FINSET_1:26;
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:12;
then
not field (RelIncl a) is empty
by A2, WELLORD1:def 7;
then
not a is empty
by WELLORD2:def 1;
then A8:
{} in a
by ORDINAL1:26, XBOOLE_1:3;
RelIncl a, RelIncl A are_isomorphic
by A1, WELLORD1:50;
then consider F being Function such that
A11:
F is_isomorphism_of RelIncl a, RelIncl A
by WELLORD1:def 8;
A12:
for m, n being Element of NAT st m in dom F & n in dom F & n < m holds
F . n in F . m
proof
let m,
n be
Element of
NAT ;
( m in dom F & n in dom F & n < m implies F . n in F . m )
assume that A13:
m in dom F
and A14:
n in dom F
and A15:
n < m
;
F . n in F . m
F . n in rng F
by A14, FUNCT_1:12;
then
F . n in field (RelIncl A)
by A11, WELLORD1:def 7;
then A16:
F . n in A
by WELLORD2:def 1;
then reconsider b =
F . n as
Element of
NAT ;
n in field (RelIncl a)
by A11, A14, WELLORD1:def 7;
then A17:
n in a
by WELLORD2:def 1;
F . m in rng F
by A13, FUNCT_1:12;
then
F . m in field (RelIncl A)
by A11, WELLORD1:def 7;
then A18:
F . m in A
by WELLORD2:def 1;
then reconsider c =
F . m as
Element of
NAT ;
n in { i where i is Element of NAT : i < m }
by A15;
then
n in m
by AXIOMS:30;
then A19:
n c= m
by ORDINAL1:def 2;
m in field (RelIncl a)
by A11, A13, WELLORD1:def 7;
then
m in a
by WELLORD2:def 1;
then
[n,m] in RelIncl a
by A17, A19, WELLORD2:def 1;
then
[(F . n),(F . m)] in RelIncl A
by A11, WELLORD1:def 7;
then A20:
F . n c= F . m
by A16, A18, WELLORD2:def 1;
F is
one-to-one
by A11, WELLORD1:def 7;
then
F . n <> F . m
by A13, A14, A15, FUNCT_1:def 8;
then
F . n c< F . m
by A20, XBOOLE_0:def 8;
then
b in c
by ORDINAL1:21;
hence
F . n in F . m
;
verum
end;
reconsider a = a as Element of NAT by A6;
dom F = field (RelIncl a)
by A11, WELLORD1:def 7;
then A21:
dom F = a
by WELLORD2:def 1;
A23:
ex m being Element of NAT st succ m = a
then consider m being Element of NAT such that
A25:
succ m = a
;
A26:
rng F = field (RelIncl A)
by A11, WELLORD1:def 7;
then A27:
rng F = A
by WELLORD2:def 1;
then reconsider F = F as Function of a,A by A21, FUNCT_2:3;
A28:
for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
F . n in F . m
by A12;
rng F = A
by A26, WELLORD2:def 1;
then A29:
F . (union a) = union (rng F)
by A23, A28, Th1;
A30:
union a = m
by A25, ORDINAL2:2;
hence
union A in A
by A27, A21, A25, A29, FUNCT_1:12, ORDINAL1:10; 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 A31:
b in A
;
( b in union A or b = union A )
now A32:
m in dom F
by A21, A25, ORDINAL1:10;
assume A33:
b <> union A
;
( b in union A or b = union A )consider c being
set such that A34:
c in dom F
and A35:
F . c = b
by A27, A31, FUNCT_1:def 5;
reconsider c =
c as
Element of
NAT by A34, ORDINAL1:19;
(
c in m or
c = m )
by A25, A34, ORDINAL1:13;
then
c in { k where k is Element of NAT : k < m }
by A27, A25, A29, A33, A35, AXIOMS:30, ORDINAL2:2;
then
ex
k being
Element of
NAT st
(
k = c &
k < m )
;
hence
(
b in union A or
b = union A )
by A12, A27, A29, A30, A34, A35, A32;
verum end;
hence
(
b in union A or
b = union A )
;
verum
end;