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 )