let M be non empty set ; :: thesis: ( ( for X being set st X in M holds

X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds

X misses Y ) implies ex Choice being set st

for X being set st X in M holds

ex x being object st Choice /\ X = {x} )

assume that

A1: for X being set st X in M holds

X <> {} and

A2: for X, Y being set st X in M & Y in M & X <> Y holds

X misses Y ; :: thesis: ex Choice being set st

for X being set st X in M holds

ex x being object st Choice /\ X = {x}

consider R being Relation such that

A3: R well_orders union M by Th11;

A4: R is_reflexive_in union M by A3;

A5: R is_connected_in union M by A3;

defpred S_{1}[ object , object ] means ex D1 being set st

( D1 = $1 & $2 in D1 & ( for z being object st z in D1 holds

[$2,z] in R ) );

A6: R is_antisymmetric_in union M by A3;

A7: for x, y, z being object st x in M & S_{1}[x,y] & S_{1}[x,z] holds

y = z

A18: for x being object st x in M holds

ex y being object st S_{1}[x,y]

A25: ( dom f = M & ( for x being object st x in M holds

S_{1}[x,f . x] ) )
from FUNCT_1:sch 2(A7, A18);

take Choice = rng f; :: thesis: for X being set st X in M holds

ex x being object st Choice /\ X = {x}

let X be set ; :: thesis: ( X in M implies ex x being object st Choice /\ X = {x} )

assume A26: X in M ; :: thesis: ex x being object st Choice /\ X = {x}

take x = f . X; :: thesis: Choice /\ X = {x}

thus Choice /\ X c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Choice /\ X

assume y in {x} ; :: thesis: y in Choice /\ X

then A32: y = x by TARSKI:def 1;

S_{1}[X,f . X]
by A25, A26;

then A33: y in X by A32;

y in Choice by A25, A26, A32, FUNCT_1:def 3;

hence y in Choice /\ X by A33, XBOOLE_0:def 4; :: thesis: verum

X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds

X misses Y ) implies ex Choice being set st

for X being set st X in M holds

ex x being object st Choice /\ X = {x} )

assume that

A1: for X being set st X in M holds

X <> {} and

A2: for X, Y being set st X in M & Y in M & X <> Y holds

X misses Y ; :: thesis: ex Choice being set st

for X being set st X in M holds

ex x being object st Choice /\ X = {x}

consider R being Relation such that

A3: R well_orders union M by Th11;

A4: R is_reflexive_in union M by A3;

A5: R is_connected_in union M by A3;

defpred S

( D1 = $1 & $2 in D1 & ( for z being object st z in D1 holds

[$2,z] in R ) );

A6: R is_antisymmetric_in union M by A3;

A7: for x, y, z being object st x in M & S

y = z

proof

A17:
R is_well_founded_in union M
by A3;
let x, y, z be object ; :: thesis: ( x in M & S_{1}[x,y] & S_{1}[x,z] implies y = z )

assume A8: x in M ; :: thesis: ( not S_{1}[x,y] or not S_{1}[x,z] or y = z )

given X being set such that A9: X = x and

A10: y in X and

A11: for u being object st u in X holds

[y,u] in R ; :: thesis: ( not S_{1}[x,z] or y = z )

A12: y in union M by A8, A10, TARSKI:def 4, A9;

given X being set such that A13: X = x and

A14: z in X and

A15: for u being object st u in X holds

[z,u] in R ; :: thesis: y = z

A16: z in union M by A8, A14, TARSKI:def 4, A13;

( [y,z] in R & [z,y] in R ) by A10, A11, A14, A15, A9, A13;

hence y = z by A6, A12, A16; :: thesis: verum

end;assume A8: x in M ; :: thesis: ( not S

given X being set such that A9: X = x and

A10: y in X and

A11: for u being object st u in X holds

[y,u] in R ; :: thesis: ( not S

A12: y in union M by A8, A10, TARSKI:def 4, A9;

given X being set such that A13: X = x and

A14: z in X and

A15: for u being object st u in X holds

[z,u] in R ; :: thesis: y = z

A16: z in union M by A8, A14, TARSKI:def 4, A13;

( [y,z] in R & [z,y] in R ) by A10, A11, A14, A15, A9, A13;

hence y = z by A6, A12, A16; :: thesis: verum

A18: for x being object st x in M holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in M implies ex y being object st S_{1}[x,y] )

assume A19: x in M ; :: thesis: ex y being object st S_{1}[x,y]

reconsider xx = x as set by TARSKI:1;

A20: xx c= union M by ZFMISC_1:74, A19;

x <> {} by A1, A19;

then consider y being object such that

A21: y in xx and

A22: R -Seg y misses xx by A17, A20;

take y ; :: thesis: S_{1}[x,y]

take xx ; :: thesis: ( xx = x & y in xx & ( for z being object st z in xx holds

[y,z] in R ) )

thus xx = x ; :: thesis: ( y in xx & ( for z being object st z in xx holds

[y,z] in R ) )

thus y in xx by A21; :: thesis: for z being object st z in xx holds

[y,z] in R

let z be object ; :: thesis: ( z in xx implies [y,z] in R )

assume A23: z in xx ; :: thesis: [y,z] in R

then A24: not z in R -Seg y by A22, XBOOLE_0:3;

( not y <> z or [y,z] in R or [z,y] in R ) by A5, A20, A21, A23;

hence [y,z] in R by A4, A20, A23, A24, WELLORD1:1; :: thesis: verum

end;assume A19: x in M ; :: thesis: ex y being object st S

reconsider xx = x as set by TARSKI:1;

A20: xx c= union M by ZFMISC_1:74, A19;

x <> {} by A1, A19;

then consider y being object such that

A21: y in xx and

A22: R -Seg y misses xx by A17, A20;

take y ; :: thesis: S

take xx ; :: thesis: ( xx = x & y in xx & ( for z being object st z in xx holds

[y,z] in R ) )

thus xx = x ; :: thesis: ( y in xx & ( for z being object st z in xx holds

[y,z] in R ) )

thus y in xx by A21; :: thesis: for z being object st z in xx holds

[y,z] in R

let z be object ; :: thesis: ( z in xx implies [y,z] in R )

assume A23: z in xx ; :: thesis: [y,z] in R

then A24: not z in R -Seg y by A22, XBOOLE_0:3;

( not y <> z or [y,z] in R or [z,y] in R ) by A5, A20, A21, A23;

hence [y,z] in R by A4, A20, A23, A24, WELLORD1:1; :: thesis: verum

A25: ( dom f = M & ( for x being object st x in M holds

S

take Choice = rng f; :: thesis: for X being set st X in M holds

ex x being object st Choice /\ X = {x}

let X be set ; :: thesis: ( X in M implies ex x being object st Choice /\ X = {x} )

assume A26: X in M ; :: thesis: ex x being object st Choice /\ X = {x}

take x = f . X; :: thesis: Choice /\ X = {x}

thus Choice /\ X c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Choice /\ X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} or y in Choice /\ X )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Choice /\ X or y in {x} )

assume A27: y in Choice /\ X ; :: thesis: y in {x}

then A28: y in X by XBOOLE_0:def 4;

y in Choice by A27, XBOOLE_0:def 4;

then consider z being object such that

A29: z in dom f and

A30: y = f . z by FUNCT_1:def 3;

reconsider z = z as set by TARSKI:1;

assume not y in {x} ; :: thesis: contradiction

then X <> z by A30, TARSKI:def 1;

then X misses z by A2, A25, A26, A29;

then A31: X /\ z = {} ;

S_{1}[z,f . z]
by A25, A29;

then f . z in z ;

hence contradiction by A28, A30, A31, XBOOLE_0:def 4; :: thesis: verum

end;assume A27: y in Choice /\ X ; :: thesis: y in {x}

then A28: y in X by XBOOLE_0:def 4;

y in Choice by A27, XBOOLE_0:def 4;

then consider z being object such that

A29: z in dom f and

A30: y = f . z by FUNCT_1:def 3;

reconsider z = z as set by TARSKI:1;

assume not y in {x} ; :: thesis: contradiction

then X <> z by A30, TARSKI:def 1;

then X misses z by A2, A25, A26, A29;

then A31: X /\ z = {} ;

S

then f . z in z ;

hence contradiction by A28, A30, A31, XBOOLE_0:def 4; :: thesis: verum

assume y in {x} ; :: thesis: y in Choice /\ X

then A32: y = x by TARSKI:def 1;

S

then A33: y in X by A32;

y in Choice by A25, A26, A32, FUNCT_1:def 3;

hence y in Choice /\ X by A33, XBOOLE_0:def 4; :: thesis: verum