Metamath Proof Explorer

Theorem metidval

Description: Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion metidval ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )

Proof

Step Hyp Ref Expression
1 df-metid ⊢ ~Met = ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } )
2 simpr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
3 2 dmeqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom 𝑑 = dom 𝐷 )
4 3 dmeqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = dom dom 𝐷 )
5 psmetdmdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
6 5 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝐷 )
7 4 6 eqtr4d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
8 7 eleq2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ dom dom 𝑑 ↔ 𝑥 ∈ 𝑋 ) )
9 7 eleq2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ dom dom 𝑑 ↔ 𝑦 ∈ 𝑋 ) )
10 8 9 anbi12d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
11 2 oveqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
12 11 eqeq1d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑦 ) = 0 ) )
13 10 12 anbi12d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ) )
14 13 opabbidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )
15 elfvunirn ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
16 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ⊆ ( 𝑋 × 𝑋 )
17 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
18 17 17 xpexd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ V )
19 ssexg ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ⊆ ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ∈ V )
20 16 18 19 sylancr ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ∈ V )
21 1 14 15 20 fvmptd2 ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )