let M be non empty set ; :: thesis: ( ( for X being set st X in M holds
X <> {} ) implies ex Choice being Function st
( dom Choice = M & ( for X being set st X in M holds
Choice . X in X ) ) )
assume A1:
for X being set st X in M holds
X <> {}
; :: thesis: ex Choice being Function st
( dom Choice = M & ( for X being set st X in M holds
Choice . X in X ) )
consider R being Relation such that
A2:
R well_orders union M
by Th26;
A3:
R is_antisymmetric_in union M
by A2, WELLORD1:def 5;
A4:
R is_well_founded_in union M
by A2, WELLORD1:def 5;
A5:
R is_connected_in union M
by A2, WELLORD1:def 5;
A6:
R is_reflexive_in union M
by A2, WELLORD1:def 5;
defpred S1[ set , set ] means ex X being set st
( $1 = X & $2 in X & ( for z being set st z in X holds
[$2,z] in R ) );
A7:
for x, y, z being set st x in M & S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
:: 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 Y being
set such that A9:
(
x = Y &
y in Y & ( for
u being
set st
u in Y holds
[y,u] in R ) )
;
:: thesis: ( not S1[x,z] or y = z )
given Z being
set such that A10:
(
x = Z &
z in Z & ( for
u being
set st
u in Z holds
[z,u] in R ) )
;
:: thesis: y = z
(
y in union M &
z in union M &
[y,z] in R &
[z,y] in R )
by A8, A9, A10, TARSKI:def 4;
hence
y = z
by A3, RELAT_2:def 4;
:: thesis: verum
end;
A11:
for x being set st x in M holds
ex y being set st S1[x,y]
proof
let x be
set ;
:: thesis: ( x in M implies ex y being set st S1[x,y] )
assume
x in M
;
:: thesis: ex y being set st S1[x,y]
then A12:
(
x c= union M &
x <> {} )
by A1, ZFMISC_1:92;
then consider y being
set such that A13:
(
y in x &
R -Seg y misses x )
by A4, WELLORD1:def 3;
A14:
(R -Seg y) /\ x = {}
by A13, XBOOLE_0:def 7;
take
y
;
:: thesis: S1[x,y]
take
x
;
:: thesis: ( x = x & y in x & ( for z being set st z in x holds
[y,z] in R ) )
thus
(
x = x &
y in x )
by A13;
:: thesis: for z being set st z in x holds
[y,z] in R
let z be
set ;
:: thesis: ( z in x implies [y,z] in R )
assume A15:
z in x
;
:: thesis: [y,z] in R
then A16:
( not
y <> z or
[y,z] in R or
[z,y] in R )
by A5, A12, A13, RELAT_2:def 6;
not
z in R -Seg y
by A14, A15, XBOOLE_0:def 4;
hence
[y,z] in R
by A6, A12, A15, A16, RELAT_2:def 1, WELLORD1:def 1;
:: thesis: verum
end;
consider f being Function such that
A17:
( dom f = M & ( for x being set st x in M holds
S1[x,f . x] ) )
from FUNCT_1:sch 2(A7, A11);
take Choice = f; :: thesis: ( dom Choice = M & ( for X being set st X in M holds
Choice . X in X ) )
thus
dom Choice = M
by A17; :: thesis: for X being set st X in M holds
Choice . X in X
let X be set ; :: thesis: ( X in M implies Choice . X in X )
assume
X in M
; :: thesis: Choice . X in X
then
ex Y being set st
( X = Y & f . X in Y & ( for z being set st z in Y holds
[(f . X),z] in R ) )
by A17;
hence
Choice . X in X
; :: thesis: verum