Metamath Proof Explorer

Theorem dfac8b

Description: The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion dfac8b 
|- ( A e. dom card -> E. x x We A )

Proof

Step Hyp Ref Expression
1 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
2 bren 
 |-  ( ( card ` A ) ~~ A <-> E. f f : ( card ` A ) -1-1-onto-> A )
3 1 2 sylib 
 |-  ( A e. dom card -> E. f f : ( card ` A ) -1-1-onto-> A )
4 sqxpexg 
 |-  ( A e. dom card -> ( A X. A ) e. _V )
5 inex2g 
 |-  ( ( A X. A ) e. _V -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) e. _V )
6 4 5 syl 
 |-  ( A e. dom card -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) e. _V )
7 f1ocnv 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> `' f : A -1-1-onto-> ( card ` A ) )
8 cardon 
 |-  ( card ` A ) e. On
9 8 onordi 
 |-  Ord ( card ` A )
10 ordwe 
 |-  ( Ord ( card ` A ) -> _E We ( card ` A ) )
11 9 10 ax-mp 
 |-  _E We ( card ` A )
12 eqid 
 |-  { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } = { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) }
13 12 f1owe 
 |-  ( `' f : A -1-1-onto-> ( card ` A ) -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A <-> _E We ( card ` A ) ) )
14 11 13 mpbiri 
 |-  ( `' f : A -1-1-onto-> ( card ` A ) -> { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A )
15 7 14 syl 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A )
16 weinxp 
 |-  ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A <-> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A )
17 15 16 sylib 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A )
18 weeq1 
 |-  ( x = ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) -> ( x We A <-> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A ) )
19 18 spcegv 
 |-  ( ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) e. _V -> ( ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A -> E. x x We A ) )
20 6 17 19 syl2im 
 |-  ( A e. dom card -> ( f : ( card ` A ) -1-1-onto-> A -> E. x x We A ) )
21 20 exlimdv 
 |-  ( A e. dom card -> ( E. f f : ( card ` A ) -1-1-onto-> A -> E. x x We A ) )
22 3 21 mpd 
 |-  ( A e. dom card -> E. x x We A )