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 f1f 
 |-  ( f : A -1-1-> y -> f : A --> y )
4 3 frnd 
 |-  ( f : A -1-1-> y -> ran f C_ y )
5 onss 
 |-  ( y e. On -> y C_ On )
6 sstr2 
 |-  ( ran f C_ y -> ( y C_ On -> ran f C_ On ) )
7 4 5 6 syl2im 
 |-  ( f : A -1-1-> y -> ( y e. On -> ran f C_ On ) )
8 epweon 
 |-  _E We On
9 wess 
 |-  ( ran f C_ On -> ( _E We On -> _E We ran f ) )
10 7 8 9 syl6mpi 
 |-  ( f : A -1-1-> y -> ( y e. On -> _E We ran f ) )
11 10 adantl 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( y e. On -> _E We ran f ) )
12 f1f1orn 
 |-  ( f : A -1-1-> y -> f : A -1-1-onto-> ran f )
13 eqid 
 |-  { <. w , z >. | ( f ` w ) _E ( f ` z ) } = { <. w , z >. | ( f ` w ) _E ( f ` z ) }
14 13 f1owe 
 |-  ( f : A -1-1-onto-> ran f -> ( _E We ran f -> { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A ) )
15 12 14 syl 
 |-  ( f : A -1-1-> y -> ( _E We ran f -> { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A ) )
16 weinxp 
 |-  ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A <-> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A )
17 reldom 
 |-  Rel ~<_
18 17 brrelex1i 
 |-  ( A ~<_ y -> A e. _V )
19 sqxpexg 
 |-  ( A e. _V -> ( A X. A ) e. _V )
20 incom 
 |-  ( ( A X. A ) i^i { <. w , z >. | ( f ` w ) _E ( f ` z ) } ) = ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) )
21 inex1g 
 |-  ( ( A X. A ) e. _V -> ( ( A X. A ) i^i { <. w , z >. | ( f ` w ) _E ( f ` z ) } ) e. _V )
22 20 21 eqeltrrid 
 |-  ( ( A X. A ) e. _V -> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) e. _V )
23 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 ) )
24 23 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 ) )
25 18 19 22 24 4syl 
 |-  ( A ~<_ y -> ( ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } i^i ( A X. A ) ) We A -> E. x x We A ) )
26 16 25 syl5bi 
 |-  ( A ~<_ y -> ( { <. w , z >. | ( f ` w ) _E ( f ` z ) } We A -> E. x x We A ) )
27 15 26 sylan9r 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( _E We ran f -> E. x x We A ) )
28 11 27 syld 
 |-  ( ( A ~<_ y /\ f : A -1-1-> y ) -> ( y e. On -> E. x x We A ) )
29 28 impancom 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( f : A -1-1-> y -> E. x x We A ) )
30 29 exlimdv 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( E. f f : A -1-1-> y -> E. x x We A ) )
31 2 30 syl5bi 
 |-  ( ( A ~<_ y /\ y e. On ) -> ( A ~<_ y -> E. x x We A ) )
32 31 ex 
 |-  ( A ~<_ y -> ( y e. On -> ( A ~<_ y -> E. x x We A ) ) )
33 32 pm2.43b 
 |-  ( y e. On -> ( A ~<_ y -> E. x x We A ) )
34 33 rexlimiv 
 |-  ( E. y e. On A ~<_ y -> E. x x We A )