Metamath Proof Explorer

Theorem pstmfval

Description: Function value of the metric induced by a pseudometric D (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis pstmval.1 ⊢ ∼ = ( ~Met ‘ 𝐷 )
Assertion pstmfval ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( [ 𝐴 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝐵 ] ∼ ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 ⊢ ∼ = ( ~Met ‘ 𝐷 )
2 1 pstmval ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) )
3 2 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) )
4 3 oveqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( [ 𝐴 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝐵 ] ∼ ) = ( [ 𝐴 ] ∼ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) [ 𝐵 ] ∼ ) )
5 1 fvexi ⊢ ∼ ∈ V
6 5 ecelqsi ⊢ ( 𝐴 ∈ 𝑋 → [ 𝐴 ] ∼ ∈ ( 𝑋 / ∼ ) )
7 6 3ad2ant2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → [ 𝐴 ] ∼ ∈ ( 𝑋 / ∼ ) )
8 5 ecelqsi ⊢ ( 𝐵 ∈ 𝑋 → [ 𝐵 ] ∼ ∈ ( 𝑋 / ∼ ) )
9 8 3ad2ant3 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → [ 𝐵 ] ∼ ∈ ( 𝑋 / ∼ ) )
10 rexeq ⊢ ( 𝑥 = [ 𝐴 ] ∼ → ( ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) ) )
11 10 abbidv ⊢ ( 𝑥 = [ 𝐴 ] ∼ → { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } = { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
12 11 unieqd ⊢ ( 𝑥 = [ 𝐴 ] ∼ → ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } = ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
13 rexeq ⊢ ( 𝑦 = [ 𝐵 ] ∼ → ( ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) )
14 13 rexbidv ⊢ ( 𝑦 = [ 𝐵 ] ∼ → ( ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) )
15 14 abbidv ⊢ ( 𝑦 = [ 𝐵 ] ∼ → { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } = { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
16 15 unieqd ⊢ ( 𝑦 = [ 𝐵 ] ∼ → ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } = ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
17 eqid ⊢ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) = ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
18 ecexg ⊢ ( ∼ ∈ V → [ 𝐴 ] ∼ ∈ V )
19 5 18 ax-mp ⊢ [ 𝐴 ] ∼ ∈ V
20 ecexg ⊢ ( ∼ ∈ V → [ 𝐵 ] ∼ ∈ V )
21 5 20 ax-mp ⊢ [ 𝐵 ] ∼ ∈ V
22 19 21 ab2rexex ⊢ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
23 22 uniex ⊢ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
24 12 16 17 23 ovmpo ⊢ ( ( [ 𝐴 ] ∼ ∈ ( 𝑋 / ∼ ) ∧ [ 𝐵 ] ∼ ∈ ( 𝑋 / ∼ ) ) → ( [ 𝐴 ] ∼ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) [ 𝐵 ] ∼ ) = ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
25 7 9 24 syl2anc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( [ 𝐴 ] ∼ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) [ 𝐵 ] ∼ ) = ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
26 simpr3 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝑧 = ( 𝑒 𝐷 𝑓 ) )
27 simpl1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
28 simpr1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝑒 ∈ [ 𝐴 ] ∼ )
29 metidss ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) ⊆ ( 𝑋 × 𝑋 ) )
30 1 29 eqsstrid ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∼ ⊆ ( 𝑋 × 𝑋 ) )
31 xpss ⊢ ( 𝑋 × 𝑋 ) ⊆ ( V × V )
32 30 31 sstrdi ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∼ ⊆ ( V × V ) )
33 df-rel ⊢ ( Rel ∼ ↔ ∼ ⊆ ( V × V ) )
34 32 33 sylibr ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → Rel ∼ )
35 34 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Rel ∼ )
36 35 adantr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → Rel ∼ )
37 relelec ⊢ ( Rel ∼ → ( 𝑒 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝑒 ) )
38 36 37 syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → ( 𝑒 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝑒 ) )
39 28 38 mpbid ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝐴 ∼ 𝑒 )
40 1 breqi ⊢ ( 𝐴 ∼ 𝑒 ↔ 𝐴 ( ~Met ‘ 𝐷 ) 𝑒 )
41 39 40 sylib ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝐴 ( ~Met ‘ 𝐷 ) 𝑒 )
42 simpr2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝑓 ∈ [ 𝐵 ] ∼ )
43 relelec ⊢ ( Rel ∼ → ( 𝑓 ∈ [ 𝐵 ] ∼ ↔ 𝐵 ∼ 𝑓 ) )
44 36 43 syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → ( 𝑓 ∈ [ 𝐵 ] ∼ ↔ 𝐵 ∼ 𝑓 ) )
45 42 44 mpbid ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝐵 ∼ 𝑓 )
46 1 breqi ⊢ ( 𝐵 ∼ 𝑓 ↔ 𝐵 ( ~Met ‘ 𝐷 ) 𝑓 )
47 45 46 sylib ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝐵 ( ~Met ‘ 𝐷 ) 𝑓 )
48 metideq ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met ‘ 𝐷 ) 𝑒 ∧ 𝐵 ( ~Met ‘ 𝐷 ) 𝑓 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑒 𝐷 𝑓 ) )
49 27 41 47 48 syl12anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑒 𝐷 𝑓 ) )
50 26 49 eqtr4d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝑧 = ( 𝐴 𝐷 𝐵 ) )
51 50 adantlr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) ∧ ( 𝑒 ∈ [ 𝐴 ] ∼ ∧ 𝑓 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) ) → 𝑧 = ( 𝐴 𝐷 𝐵 ) )
52 51 3anassrs ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) ∧ 𝑒 ∈ [ 𝐴 ] ∼ ) ∧ 𝑓 ∈ [ 𝐵 ] ∼ ) ∧ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) → 𝑧 = ( 𝐴 𝐷 𝐵 ) )
53 oveq1 ⊢ ( 𝑎 = 𝑒 → ( 𝑎 𝐷 𝑏 ) = ( 𝑒 𝐷 𝑏 ) )
54 53 eqeq2d ⊢ ( 𝑎 = 𝑒 → ( 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ 𝑧 = ( 𝑒 𝐷 𝑏 ) ) )
55 oveq2 ⊢ ( 𝑏 = 𝑓 → ( 𝑒 𝐷 𝑏 ) = ( 𝑒 𝐷 𝑓 ) )
56 55 eqeq2d ⊢ ( 𝑏 = 𝑓 → ( 𝑧 = ( 𝑒 𝐷 𝑏 ) ↔ 𝑧 = ( 𝑒 𝐷 𝑓 ) ) )
57 54 56 cbvrex2vw ⊢ ( ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ ∃ 𝑒 ∈ [ 𝐴 ] ∼ ∃ 𝑓 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑒 𝐷 𝑓 ) )
58 57 biimpi ⊢ ( ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) → ∃ 𝑒 ∈ [ 𝐴 ] ∼ ∃ 𝑓 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑒 𝐷 𝑓 ) )
59 58 adantl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) → ∃ 𝑒 ∈ [ 𝐴 ] ∼ ∃ 𝑓 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑒 𝐷 𝑓 ) )
60 52 59 r19.29vva ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ) → 𝑧 = ( 𝐴 𝐷 𝐵 ) )
61 simpl1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
62 simpl2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝐴 ∈ 𝑋 )
63 psmet0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 0 )
64 61 62 63 syl2anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 𝐷 𝐴 ) = 0 )
65 relelec ⊢ ( Rel ∼ → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
66 61 34 65 3syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
67 1 a1i ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ∼ = ( ~Met ‘ 𝐷 ) )
68 67 breqd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 ∼ 𝐴 ↔ 𝐴 ( ~Met ‘ 𝐷 ) 𝐴 ) )
69 metidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐴 ( ~Met ‘ 𝐷 ) 𝐴 ↔ ( 𝐴 𝐷 𝐴 ) = 0 ) )
70 61 62 62 69 syl12anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 ( ~Met ‘ 𝐷 ) 𝐴 ↔ ( 𝐴 𝐷 𝐴 ) = 0 ) )
71 66 68 70 3bitrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ ( 𝐴 𝐷 𝐴 ) = 0 ) )
72 64 71 mpbird ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝐴 ∈ [ 𝐴 ] ∼ )
73 simpl3 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝐵 ∈ 𝑋 )
74 psmet0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
75 61 73 74 syl2anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐵 𝐷 𝐵 ) = 0 )
76 relelec ⊢ ( Rel ∼ → ( 𝐵 ∈ [ 𝐵 ] ∼ ↔ 𝐵 ∼ 𝐵 ) )
77 61 34 76 3syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐵 ∈ [ 𝐵 ] ∼ ↔ 𝐵 ∼ 𝐵 ) )
78 67 breqd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐵 ∼ 𝐵 ↔ 𝐵 ( ~Met ‘ 𝐷 ) 𝐵 ) )
79 metidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ( ~Met ‘ 𝐷 ) 𝐵 ↔ ( 𝐵 𝐷 𝐵 ) = 0 ) )
80 61 73 73 79 syl12anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐵 ( ~Met ‘ 𝐷 ) 𝐵 ↔ ( 𝐵 𝐷 𝐵 ) = 0 ) )
81 77 78 80 3bitrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ( 𝐵 ∈ [ 𝐵 ] ∼ ↔ ( 𝐵 𝐷 𝐵 ) = 0 ) )
82 75 81 mpbird ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝐵 ∈ [ 𝐵 ] ∼ )
83 simpr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → 𝑧 = ( 𝐴 𝐷 𝐵 ) )
84 rspceov ⊢ ( ( 𝐴 ∈ [ 𝐴 ] ∼ ∧ 𝐵 ∈ [ 𝐵 ] ∼ ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) )
85 72 82 83 84 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) → ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) )
86 60 85 impbida ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) ↔ 𝑧 = ( 𝐴 𝐷 𝐵 ) ) )
87 86 abbidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } = { 𝑧 ∣ 𝑧 = ( 𝐴 𝐷 𝐵 ) } )
88 df-sn ⊢ { ( 𝐴 𝐷 𝐵 ) } = { 𝑧 ∣ 𝑧 = ( 𝐴 𝐷 𝐵 ) }
89 87 88 eqtr4di ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } = { ( 𝐴 𝐷 𝐵 ) } )
90 89 unieqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } = ∪ { ( 𝐴 𝐷 𝐵 ) } )
91 ovex ⊢ ( 𝐴 𝐷 𝐵 ) ∈ V
92 91 unisn ⊢ ∪ { ( 𝐴 𝐷 𝐵 ) } = ( 𝐴 𝐷 𝐵 )
93 90 92 eqtrdi ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∪ { 𝑧 ∣ ∃ 𝑎 ∈ [ 𝐴 ] ∼ ∃ 𝑏 ∈ [ 𝐵 ] ∼ 𝑧 = ( 𝑎 𝐷 𝑏 ) } = ( 𝐴 𝐷 𝐵 ) )
94 4 25 93 3eqtrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( [ 𝐴 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝐵 ] ∼ ) = ( 𝐴 𝐷 𝐵 ) )