This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 incom 
 |-  ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) = ( ( A X. A ) i^i { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } )
6 inex1g 
 |-  ( ( A X. A ) e. _V -> ( ( A X. A ) i^i { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } ) e. _V )
7 5 6 eqeltrid 
 |-  ( ( A X. A ) e. _V -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) e. _V )
8 4 7 syl 
 |-  ( A e. dom card -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) e. _V )
9 f1ocnv 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> `' f : A -1-1-onto-> ( card ` A ) )
10 cardon 
 |-  ( card ` A ) e. On
11 10 onordi 
 |-  Ord ( card ` A )
12 ordwe 
 |-  ( Ord ( card ` A ) -> _E We ( card ` A ) )
13 11 12 ax-mp 
 |-  _E We ( card ` A )
14 eqid 
 |-  { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } = { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) }
15 14 f1owe 
 |-  ( `' f : A -1-1-onto-> ( card ` A ) -> ( _E We ( card ` A ) -> { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A ) )
16 9 13 15 mpisyl 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A )
17 weinxp 
 |-  ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } We A <-> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A )
18 16 17 sylib 
 |-  ( f : ( card ` A ) -1-1-onto-> A -> ( { <. z , w >. | ( `' f ` z ) _E ( `' f ` w ) } i^i ( A X. A ) ) We A )
19 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 ) )
20 19 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 ) )
21 8 18 20 syl2im 
 |-  ( A e. dom card -> ( f : ( card ` A ) -1-1-onto-> A -> E. x x We A ) )
22 21 exlimdv 
 |-  ( A e. dom card -> ( E. f f : ( card ` A ) -1-1-onto-> A -> E. x x We A ) )
23 3 22 mpd 
 |-  ( A e. dom card -> E. x x We A )