Metamath Proof Explorer

Theorem ac10ct

Description: A proof of the well-ordering theorem weth , an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion ac10ct 
|- ( E. y e. On A ~<_ y -> E. x x We A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 1 brdom 
 |-  ( A ~<_ y <-> E. f f : A -1-1-> y )
3 onss 
 |-  ( y e. On -> y C_ On )
4 3 a1i 
 |-  ( f : A -1-1-> y -> ( y e. On -> y C_ On ) )
5 epweon 
 |-  _E We On
6 wess 
 |-  ( y C_ On -> ( _E We On -> _E We y ) )
7 4 5 6 syl6mpi 
 |-  ( f : A -1-1-> y -> ( y e. On -> _E We y ) )
8 7 adantl 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( y e. On -> _E We y ) )
9 eqid 
 |-  { <. w , z >. | ( f ` w ) _E ( f ` z ) } = { <. w , z >. | ( f ` w ) _E ( f ` z ) }
10 9 f1we 
 |-  ( f : A -1-1-> y -> ( _E We y -> { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A ) )
11 weinxp 
 |-  ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A <-> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A )
12 reldom 
 |-  Rel ~<_
13 12 brrelex1i 
 |-  ( A ~<_ y -> A e. _V )
14 sqxpexg 
 |-  ( A e. _V -> ( A X. A ) e. _V )
15 inex2g 
 |-  ( ( A X. A ) e. _V -> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) e. _V )
16 weeq1 
 |-  ( x = ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) -> ( x We A <-> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A ) )
17 16 spcegv 
 |-  ( ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) e. _V -> ( ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A -> E. x x We A ) )
18 13 14 15 17 4syl 
 |-  ( A ~<_ y -> ( ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A -> E. x x We A ) )
19 11 18 biimtrid 
 |-  ( A ~<_ y -> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A -> E. x x We A ) )
20 10 19 sylan9r 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( _E We y -> E. x x We A ) )
21 8 20 syld 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( y e. On -> E. x x We A ) )
22 21 impancom 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( f : A -1-1-> y -> E. x x We A ) )
23 22 exlimdv 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( E. f f : A -1-1-> y -> E. x x We A ) )
24 2 23 biimtrid 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( A ~<_ y -> E. x x We A ) )
25 24 ex 
 |-  ( A ~<_ y -> ( y e. On -> ( A ~<_ y -> E. x x We A ) ) )
26 25 pm2.43b 
 |-  ( y e. On -> ( A ~<_ y -> E. x x We A ) )
27 26 rexlimiv 
 |-  ( E. y e. On A ~<_ y -> E. x x We A )