deffunc H1( set ) -> set = $1 `2 ;
set x = the Element of M;
deffunc H2( set ) -> set = [:{$1},$1:];
consider f being Function such that
A2:
dom f = M
and
A3:
for X being set st X in M holds
f . X = H2(X)
from FUNCT_1:sch 3();
A4:
the Element of M in M
;
then reconsider N = rng f as non empty set by A2, FUNCT_1:3;
A5:
now let X,
Y be
set ;
( X in N & Y in N & X <> Y implies not X meets Y )assume that A6:
X in N
and A7:
Y in N
and A8:
X <> Y
;
not X meets Yconsider y being
set such that A9:
y in dom f
and A10:
f . y = Y
by A7, FUNCT_1:def 3;
A11:
Y = [:{y},y:]
by A2, A3, A9, A10;
set z = the
Element of
X /\ Y;
assume
X meets Y
;
contradictionthen A12:
X /\ Y <> {}
by XBOOLE_0:def 7;
consider x being
set such that A13:
x in dom f
and A14:
f . x = X
by A6, FUNCT_1:def 3;
X = [:{x},x:]
by A2, A3, A13, A14;
then consider x1,
x2 being
set such that
the
Element of
X /\ Y = [x1,x2]
and A15:
x1 in {x} /\ {y}
and
x2 in x /\ y
by A11, A12, ZFMISC_1:85;
x1 in {x}
by A15, XBOOLE_0:def 4;
then A16:
x1 = x
by TARSKI:def 1;
x1 in {y}
by A15, XBOOLE_0:def 4;
hence
contradiction
by A8, A14, A10, A16, TARSKI:def 1;
verum end;
then consider Choice being set such that
A20:
for X being set st X in N holds
ex x being set st Choice /\ X = {x}
by A5, WELLORD2:18;
defpred S1[ set , set ] means $2 in $1 /\ Choice;
A21:
for X being set st X in N holds
ex y being set st S1[X,y]
proof
let X be
set ;
( X in N implies ex y being set st S1[X,y] )
assume
X in N
;
ex y being set st S1[X,y]
then consider x being
set such that A22:
Choice /\ X = {x}
by A20;
take
x
;
S1[X,x]
thus
S1[
X,
x]
by A22, TARSKI:def 1;
verum
end;
A23:
for X, y1, y2 being set st X in N & S1[X,y1] & S1[X,y2] holds
y1 = y2
consider g being Function such that
A28:
dom g = N
and
A29:
for X being set st X in N holds
S1[X,g . X]
from FUNCT_1:sch 2(A23, A21);
A30:
rng g c= union N
f . the Element of M in rng f
by A2, FUNCT_1:def 3;
then consider x1 being set such that
A33:
x1 in N
;
consider x2 being set such that
A34:
x2 in dom f
and
A35:
f . x2 = x1
by A33, FUNCT_1:def 3;
A36:
x2 <> {}
by A1, A2, A34;
reconsider f = f as Function of M,N by A2, FUNCT_2:def 1, RELSET_1:4;
consider h being Function such that
A37:
dom h = union N
and
A38:
for x being set st x in union N holds
h . x = H1(x)
from FUNCT_1:sch 3();
A39:
rng h c= union M
proof
let x be
set ;
TARSKI:def 3 ( not x in rng h or x in union M )
assume
x in rng h
;
x in union M
then consider y being
set such that A40:
y in dom h
and A41:
h . y = x
by FUNCT_1:def 3;
consider Y being
set such that A42:
y in Y
and A43:
Y in N
by A37, A40, TARSKI:def 4;
consider z being
set such that A44:
z in dom f
and A45:
f . z = Y
by A43, FUNCT_1:def 3;
A46:
Y = [:{z},z:]
by A3, A44, A45;
then consider x1,
x2 being
set such that A47:
y = [x1,x2]
by A42, RELAT_1:def 1;
A48:
x2 in z
by A42, A46, A47, ZFMISC_1:87;
x = [x1,x2] `2
by A37, A38, A40, A41, A47;
then
x in z
by A48, MCART_1:7;
hence
x in union M
by A44, TARSKI:def 4;
verum
end;
x1 = [:{x2},x2:]
by A2, A3, A34, A35;
then A49:
union N <> {}
by A33, A36, Lm1;
then reconsider g = g as Function of N,(union N) by A28, A30, FUNCT_2:def 1, RELSET_1:4;
union M <> {}
by A1, A4, Lm1;
then reconsider h = h as Function of (union N),(union M) by A37, A39, FUNCT_2:def 1, RELSET_1:4;
A50:
dom (g * f) = M
by A49, FUNCT_2:def 1;
reconsider F = h * (g * f) as Function of M,(union M) by A49;
take
F
; for X being set st X in M holds
F . X in X
let X be set ; ( X in M implies F . X in X )
assume A51:
X in M
; F . X in X
then A52:
f . X = [:{X},X:]
by A3;
set fX = f . X;
A53:
f . X in N
by A2, A51, FUNCT_1:def 3;
then
g . (f . X) in rng g
by A28, FUNCT_1:def 3;
then A54:
h . (g . (f . X)) = (g . (f . X)) `2
by A38;
A55:
g . (f . X) in (f . X) /\ Choice
by A29, A53;
then consider x1, x2 being set such that
A56:
[x1,x2] = g . (f . X)
by A52, RELAT_1:def 1;
g . (f . X) in f . X
by A55, XBOOLE_0:def 4;
then
x2 in X
by A52, A56, ZFMISC_1:87;
then A57:
h . (g . (f . X)) in X
by A56, A54, MCART_1:7;
(g * f) . X = g . (f . X)
by A2, A51, FUNCT_1:13;
hence
F . X in X
by A50, A51, A57, FUNCT_1:13; verum