Metamath Proof Explorer

Theorem dnwech

Description: Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f 
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
dnnumch.a 
|- ( ph -> A e. V )
dnnumch.g 
|- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
dnwech.h 
|- H = { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) }
Assertion dnwech 
|- ( ph -> H We A )

Proof

Step Hyp Ref Expression
1 dnnumch.f 
 |-  F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
2 dnnumch.a 
 |-  ( ph -> A e. V )
3 dnnumch.g 
 |-  ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
4 dnwech.h 
 |-  H = { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) }
5 1 2 3 dnnumch3 
 |-  ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On )
6 f1f1orn 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-onto-> ran ( x e. A |-> |^| ( `' F " { x } ) ) )
7 5 6 syl 
 |-  ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-onto-> ran ( x e. A |-> |^| ( `' F " { x } ) ) )
8 f1f 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On -> ( x e. A |-> |^| ( `' F " { x } ) ) : A --> On )
9 frn 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A --> On -> ran ( x e. A |-> |^| ( `' F " { x } ) ) C_ On )
10 5 8 9 3syl 
 |-  ( ph -> ran ( x e. A |-> |^| ( `' F " { x } ) ) C_ On )
11 epweon 
 |-  _E We On
12 wess 
 |-  ( ran ( x e. A |-> |^| ( `' F " { x } ) ) C_ On -> ( _E We On -> _E We ran ( x e. A |-> |^| ( `' F " { x } ) ) ) )
13 10 11 12 mpisyl 
 |-  ( ph -> _E We ran ( x e. A |-> |^| ( `' F " { x } ) ) )
14 eqid 
 |-  { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } = { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) }
15 14 f1owe 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-onto-> ran ( x e. A |-> |^| ( `' F " { x } ) ) -> ( _E We ran ( x e. A |-> |^| ( `' F " { x } ) ) -> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A ) )
16 7 13 15 sylc 
 |-  ( ph -> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A )
17 fvex 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) e. _V
18 17 epeli 
 |-  ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) <-> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) e. ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) )
19 1 2 3 dnnumch3lem 
 |-  ( ( ph /\ v e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )
20 19 adantrr 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )
21 1 2 3 dnnumch3lem 
 |-  ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
22 21 adantrl 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
23 20 22 eleq12d 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) e. ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) <-> |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) )
24 18 23 bitr2id 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) <-> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) ) )
25 24 pm5.32da 
 |-  ( ph -> ( ( ( v e. A /\ w e. A ) /\ |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) <-> ( ( v e. A /\ w e. A ) /\ ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) ) ) )
26 25 opabbidv 
 |-  ( ph -> { <. v , w >. | ( ( v e. A /\ w e. A ) /\ |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) } = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) ) } )
27 incom 
 |-  ( H i^i ( A X. A ) ) = ( ( A X. A ) i^i H )
28 df-xp 
 |-  ( A X. A ) = { <. v , w >. | ( v e. A /\ w e. A ) }
29 28 4 ineq12i 
 |-  ( ( A X. A ) i^i H ) = ( { <. v , w >. | ( v e. A /\ w e. A ) } i^i { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) } )
30 inopab 
 |-  ( { <. v , w >. | ( v e. A /\ w e. A ) } i^i { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) } ) = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) }
31 27 29 30 3eqtri 
 |-  ( H i^i ( A X. A ) ) = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) }
32 incom 
 |-  ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) = ( ( A X. A ) i^i { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } )
33 28 ineq1i 
 |-  ( ( A X. A ) i^i { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } ) = ( { <. v , w >. | ( v e. A /\ w e. A ) } i^i { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } )
34 inopab 
 |-  ( { <. v , w >. | ( v e. A /\ w e. A ) } i^i { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } ) = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) ) }
35 32 33 34 3eqtri 
 |-  ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) ) }
36 26 31 35 3eqtr4g 
 |-  ( ph -> ( H i^i ( A X. A ) ) = ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) )
37 weeq1 
 |-  ( ( H i^i ( A X. A ) ) = ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) -> ( ( H i^i ( A X. A ) ) We A <-> ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) We A ) )
38 36 37 syl 
 |-  ( ph -> ( ( H i^i ( A X. A ) ) We A <-> ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) We A ) )
39 weinxp 
 |-  ( H We A <-> ( H i^i ( A X. A ) ) We A )
40 weinxp 
 |-  ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A <-> ( { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } i^i ( A X. A ) ) We A )
41 38 39 40 3bitr4g 
 |-  ( ph -> ( H We A <-> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A ) )
42 16 41 mpbird 
 |-  ( ph -> H We A )