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 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
dnnumch.a ( 𝜑𝐴𝑉 )
dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
dnwech.h 𝐻 = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) }
Assertion dnwech ( 𝜑𝐻 We 𝐴 )

Proof

Step Hyp Ref Expression
1 dnnumch.f 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2 dnnumch.a ( 𝜑𝐴𝑉 )
3 dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
4 dnwech.h 𝐻 = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) }
5 1 2 3 dnnumch3 ( 𝜑 → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1→ On )
6 f1f1orn ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1→ On → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) )
7 5 6 syl ( 𝜑 → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) )
8 f1f ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1→ On → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On )
9 frn ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On → ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ⊆ On )
10 5 8 9 3syl ( 𝜑 → ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ⊆ On )
11 epweon E We On
12 wess ( ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ⊆ On → ( E We On → E We ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ) )
13 10 11 12 mpisyl ( 𝜑 → E We ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) )
14 eqid { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) }
15 14 f1owe ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1-onto→ ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) → ( E We ran ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ) )
16 7 13 15 sylc ( 𝜑 → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 )
17 fvex ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ∈ V
18 17 epeli ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) ∈ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) )
19 1 2 3 dnnumch3lem ( ( 𝜑𝑣𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( 𝐹 “ { 𝑣 } ) )
20 19 adantrr ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( 𝐹 “ { 𝑣 } ) )
21 1 2 3 dnnumch3lem ( ( 𝜑𝑤𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )
22 21 adantrl ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )
23 20 22 eleq12d ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) ∈ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ) )
24 18 23 bitr2id ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ↔ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) )
25 24 pm5.32da ( 𝜑 → ( ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ) ↔ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) ) )
26 25 opabbidv ( 𝜑 → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) } )
27 incom ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ 𝐻 )
28 df-xp ( 𝐴 × 𝐴 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣𝐴𝑤𝐴 ) }
29 28 4 ineq12i ( ( 𝐴 × 𝐴 ) ∩ 𝐻 ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣𝐴𝑤𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) } )
30 inopab ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣𝐴𝑤𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) } ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ) }
31 27 29 30 3eqtri ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑤 } ) ) }
32 incom ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } )
33 28 ineq1i ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣𝐴𝑤𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } )
34 inopab ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣𝐴𝑤𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) }
35 32 33 34 3eqtri ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣𝐴𝑤𝐴 ) ∧ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) }
36 26 31 35 3eqtr4g ( 𝜑 → ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) )
37 weeq1 ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
38 36 37 syl ( 𝜑 → ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
39 weinxp ( 𝐻 We 𝐴 ↔ ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
40 weinxp ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
41 38 39 40 3bitr4g ( 𝜑 → ( 𝐻 We 𝐴 ↔ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ) )
42 16 41 mpbird ( 𝜑𝐻 We 𝐴 )