# 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 } ) )`
` |-  ( ( 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 } ) )`
` |-  ( ( 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 syl5rbb
` |-  ( ( 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 )`