| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pstmval.1 | . . . . 5
⊢  ∼ =
(~Met‘𝐷) | 
| 2 | 1 | pstmval 33894 | . . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) | 
| 3 | 2 | 3ad2ant1 1134 | . . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) | 
| 4 | 3 | oveqd 7448 | . 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ )) | 
| 5 | 1 | fvexi 6920 | . . . . 5
⊢  ∼ ∈
V | 
| 6 | 5 | ecelqsi 8813 | . . . 4
⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ ∈ (𝑋 / ∼ )) | 
| 7 | 6 | 3ad2ant2 1135 | . . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐴] ∼ ∈ (𝑋 / ∼ )) | 
| 8 | 5 | ecelqsi 8813 | . . . 4
⊢ (𝐵 ∈ 𝑋 → [𝐵] ∼ ∈ (𝑋 / ∼ )) | 
| 9 | 8 | 3ad2ant3 1136 | . . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐵] ∼ ∈ (𝑋 / ∼ )) | 
| 10 |  | rexeq 3322 | . . . . . 6
⊢ (𝑥 = [𝐴] ∼ →
(∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏))) | 
| 11 | 10 | abbidv 2808 | . . . . 5
⊢ (𝑥 = [𝐴] ∼ → {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) | 
| 12 | 11 | unieqd 4920 | . . . 4
⊢ (𝑥 = [𝐴] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) | 
| 13 |  | rexeq 3322 | . . . . . . 7
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) | 
| 14 | 13 | rexbidv 3179 | . . . . . 6
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) | 
| 15 | 14 | abbidv 2808 | . . . . 5
⊢ (𝑦 = [𝐵] ∼ → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) | 
| 16 | 15 | unieqd 4920 | . . . 4
⊢ (𝑦 = [𝐵] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) | 
| 17 |  | eqid 2737 | . . . 4
⊢ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) | 
| 18 |  | ecexg 8749 | . . . . . . 7
⊢ ( ∼ ∈
V → [𝐴] ∼ ∈
V) | 
| 19 | 5, 18 | ax-mp 5 | . . . . . 6
⊢ [𝐴] ∼ ∈
V | 
| 20 |  | ecexg 8749 | . . . . . . 7
⊢ ( ∼ ∈
V → [𝐵] ∼ ∈
V) | 
| 21 | 5, 20 | ax-mp 5 | . . . . . 6
⊢ [𝐵] ∼ ∈
V | 
| 22 | 19, 21 | ab2rexex 8004 | . . . . 5
⊢ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V | 
| 23 | 22 | uniex 7761 | . . . 4
⊢ ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V | 
| 24 | 12, 16, 17, 23 | ovmpo 7593 | . . 3
⊢ (([𝐴] ∼ ∈ (𝑋 / ∼ ) ∧ [𝐵] ∼ ∈ (𝑋 / ∼ )) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) | 
| 25 | 7, 9, 24 | syl2anc 584 | . 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) | 
| 26 |  | simpr3 1197 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝑒𝐷𝑓)) | 
| 27 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐷 ∈ (PsMet‘𝑋)) | 
| 28 |  | simpr1 1195 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑒 ∈ [𝐴] ∼ ) | 
| 29 |  | metidss 33890 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (𝑋 × 𝑋)) | 
| 30 | 1, 29 | eqsstrid 4022 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (𝑋 × 𝑋)) | 
| 31 |  | xpss 5701 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 × 𝑋) ⊆ (V × V) | 
| 32 | 30, 31 | sstrdi 3996 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (V ×
V)) | 
| 33 |  | df-rel 5692 | . . . . . . . . . . . . . . . . . 18
⊢ (Rel
∼
↔ ∼ ⊆ (V ×
V)) | 
| 34 | 32, 33 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (PsMet‘𝑋) → Rel ∼ ) | 
| 35 | 34 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Rel ∼ ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → Rel ∼ ) | 
| 37 |  | relelec 8792 | . . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) | 
| 39 | 28, 38 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴 ∼ 𝑒) | 
| 40 | 1 | breqi 5149 | . . . . . . . . . . . . 13
⊢ (𝐴 ∼ 𝑒 ↔ 𝐴(~Met‘𝐷)𝑒) | 
| 41 | 39, 40 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴(~Met‘𝐷)𝑒) | 
| 42 |  | simpr2 1196 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑓 ∈ [𝐵] ∼ ) | 
| 43 |  | relelec 8792 | . . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) | 
| 44 | 36, 43 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) | 
| 45 | 42, 44 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵 ∼ 𝑓) | 
| 46 | 1 | breqi 5149 | . . . . . . . . . . . . 13
⊢ (𝐵 ∼ 𝑓 ↔ 𝐵(~Met‘𝐷)𝑓) | 
| 47 | 45, 46 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵(~Met‘𝐷)𝑓) | 
| 48 |  | metideq 33892 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝑒 ∧ 𝐵(~Met‘𝐷)𝑓)) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) | 
| 49 | 27, 41, 47, 48 | syl12anc 837 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) | 
| 50 | 26, 49 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) | 
| 51 | 50 | adantlr 715 | . . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) | 
| 52 | 51 | 3anassrs 1361 | . . . . . . . 8
⊢
((((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ 𝑒 ∈ [𝐴] ∼ ) ∧ 𝑓 ∈ [𝐵] ∼ ) ∧ 𝑧 = (𝑒𝐷𝑓)) → 𝑧 = (𝐴𝐷𝐵)) | 
| 53 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑒 → (𝑎𝐷𝑏) = (𝑒𝐷𝑏)) | 
| 54 | 53 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑒 → (𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑏))) | 
| 55 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑓 → (𝑒𝐷𝑏) = (𝑒𝐷𝑓)) | 
| 56 | 55 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑓 → (𝑧 = (𝑒𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑓))) | 
| 57 | 54, 56 | cbvrex2vw 3242 | . . . . . . . . . 10
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) | 
| 58 | 57 | biimpi 216 | . . . . . . . . 9
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) | 
| 59 | 58 | adantl 481 | . . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) | 
| 60 | 52, 59 | r19.29vva 3216 | . . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → 𝑧 = (𝐴𝐷𝐵)) | 
| 61 |  | simpl1 1192 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐷 ∈ (PsMet‘𝑋)) | 
| 62 |  | simpl2 1193 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ 𝑋) | 
| 63 |  | psmet0 24318 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) | 
| 64 | 61, 62, 63 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴𝐷𝐴) = 0) | 
| 65 |  | relelec 8792 | . . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) | 
| 66 | 61, 34, 65 | 3syl 18 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) | 
| 67 | 1 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∼ =
(~Met‘𝐷)) | 
| 68 | 67 | breqd 5154 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∼ 𝐴 ↔ 𝐴(~Met‘𝐷)𝐴)) | 
| 69 |  | metidv 33891 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) | 
| 70 | 61, 62, 62, 69 | syl12anc 837 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) | 
| 71 | 66, 68, 70 | 3bitrd 305 | . . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ (𝐴𝐷𝐴) = 0)) | 
| 72 | 64, 71 | mpbird 257 | . . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ [𝐴] ∼ ) | 
| 73 |  | simpl3 1194 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ 𝑋) | 
| 74 |  | psmet0 24318 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵 ∈ 𝑋) → (𝐵𝐷𝐵) = 0) | 
| 75 | 61, 73, 74 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵𝐷𝐵) = 0) | 
| 76 |  | relelec 8792 | . . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) | 
| 77 | 61, 34, 76 | 3syl 18 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) | 
| 78 | 67 | breqd 5154 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∼ 𝐵 ↔ 𝐵(~Met‘𝐷)𝐵)) | 
| 79 |  | metidv 33891 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) | 
| 80 | 61, 73, 73, 79 | syl12anc 837 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) | 
| 81 | 77, 78, 80 | 3bitrd 305 | . . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ (𝐵𝐷𝐵) = 0)) | 
| 82 | 75, 81 | mpbird 257 | . . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ [𝐵] ∼ ) | 
| 83 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝑧 = (𝐴𝐷𝐵)) | 
| 84 |  | rspceov 7480 | . . . . . . . 8
⊢ ((𝐴 ∈ [𝐴] ∼ ∧ 𝐵 ∈ [𝐵] ∼ ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) | 
| 85 | 72, 82, 83, 84 | syl3anc 1373 | . . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) | 
| 86 | 60, 85 | impbida 801 | . . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝐴𝐷𝐵))) | 
| 87 | 86 | abbidv 2808 | . . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)}) | 
| 88 |  | df-sn 4627 | . . . . 5
⊢ {(𝐴𝐷𝐵)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)} | 
| 89 | 87, 88 | eqtr4di 2795 | . . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {(𝐴𝐷𝐵)}) | 
| 90 | 89 | unieqd 4920 | . . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = ∪ {(𝐴𝐷𝐵)}) | 
| 91 |  | ovex 7464 | . . . 4
⊢ (𝐴𝐷𝐵) ∈ V | 
| 92 | 91 | unisn 4926 | . . 3
⊢ ∪ {(𝐴𝐷𝐵)} = (𝐴𝐷𝐵) | 
| 93 | 90, 92 | eqtrdi 2793 | . 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = (𝐴𝐷𝐵)) | 
| 94 | 4, 25, 93 | 3eqtrd 2781 | 1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) |