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 epweon 
 |-  _E We On
7 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 ) }
8 7 f1we 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On -> ( _E We On -> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A ) )
9 5 6 8 mpisyl 
 |-  ( ph -> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A )
10 fvex 
 |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) e. _V
11 10 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 ) )
12 1 2 3 dnnumch3lem 
 |-  ( ( ph /\ v e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )
13 12 adantrr 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )
14 1 2 3 dnnumch3lem 
 |-  ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
15 14 adantrl 
 |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
16 13 15 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 } ) ) )
17 11 16 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 ) ) )
18 17 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 ) ) ) )
19 18 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 ) ) } )
20 incom 
 |-  ( H i^i ( A X. A ) ) = ( ( A X. A ) i^i H )
21 df-xp 
 |-  ( A X. A ) = { <. v , w >. | ( v e. A /\ w e. A ) }
22 21 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 } ) } )
23 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 } ) ) }
24 20 22 23 3eqtri 
 |-  ( H i^i ( A X. A ) ) = { <. v , w >. | ( ( v e. A /\ w e. A ) /\ |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) ) }
25 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 ) } )
26 21 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 ) } )
27 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 ) ) }
28 25 26 27 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 ) ) }
29 19 24 28 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 ) ) )
30 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 ) )
31 29 30 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 ) )
32 weinxp 
 |-  ( H We A <-> ( H i^i ( A X. A ) ) We A )
33 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 )
34 31 32 33 3bitr4g 
 |-  ( ph -> ( H We A <-> { <. v , w >. | ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) _E ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) } We A ) )
35 9 34 mpbird 
 |-  ( ph -> H We A )