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 S1[ 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 & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( x in M & S1[x,y] & S1[x,z] implies y = z )
assume A8: x in M ; :: thesis: ( not S1[x,y] or not S1[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 S1[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;
A17: R is_well_founded_in union M by A3;
A18: for x being object st x in M holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in M implies ex y being object st S1[x,y] )
assume A19: x in M ; :: thesis: ex y being object st S1[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: S1[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;
consider f being Function such that
A25: ( dom f = M & ( for x being object st x in M holds
S1[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
proof
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 = {} ;
S1[z,f . z] by A25, A29;
then f . z in z ;
hence contradiction by A28, A30, A31, XBOOLE_0:def 4; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} or y in Choice /\ X )
assume y in {x} ; :: thesis: y in Choice /\ X
then A32: y = x by TARSKI:def 1;
S1[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