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 epweon ⊢ E We On
7 eqid ⊢ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) }
8 7 f1we ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On → ( E We On → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ) )
9 5 6 8 mpisyl ⊢ ( 𝜑 → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 )
10 fvex ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ∈ V
11 10 epeli ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) )
12 1 2 3 dnnumch3lem ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
13 12 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
14 1 2 3 dnnumch3lem ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
15 14 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
16 13 15 eleq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
17 11 16 bitr2id ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) )
18 17 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) ↔ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) ) )
19 18 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) } )
20 incom ⊢ ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ 𝐻 )
21 df-xp ⊢ ( 𝐴 × 𝐴 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) }
22 21 4 ineq12i ⊢ ( ( 𝐴 × 𝐴 ) ∩ 𝐻 ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) } )
23 inopab ⊢ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) } ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) }
24 20 22 23 3eqtri ⊢ ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) }
25 incom ⊢ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } )
26 21 ineq1i ⊢ ( ( 𝐴 × 𝐴 ) ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } )
27 inopab ⊢ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) } ∩ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) }
28 25 26 27 3eqtri ⊢ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ) }
29 19 24 28 3eqtr4g ⊢ ( 𝜑 → ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) )
30 weeq1 ⊢ ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) = ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
31 29 30 syl ⊢ ( 𝜑 → ( ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
32 weinxp ⊢ ( 𝐻 We 𝐴 ↔ ( 𝐻 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
33 weinxp ⊢ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ↔ ( { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
34 31 32 33 3bitr4g ⊢ ( 𝜑 → ( 𝐻 We 𝐴 ↔ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) E ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) } We 𝐴 ) )
35 9 34 mpbird ⊢ ( 𝜑 → 𝐻 We 𝐴 )