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 syl5rbb ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) 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 𝐴 )