Step | Hyp | Ref
| Expression |
1 | | pstmval.1 |
. . . . 5
⊢ ∼ =
(~Met‘𝐷) |
2 | 1 | pstmval 31419 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) |
3 | 2 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) |
4 | 3 | oveqd 7189 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ )) |
5 | 1 | fvexi 6690 |
. . . . 5
⊢ ∼ ∈
V |
6 | 5 | ecelqsi 8386 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ ∈ (𝑋 / ∼ )) |
7 | 6 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐴] ∼ ∈ (𝑋 / ∼ )) |
8 | 5 | ecelqsi 8386 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → [𝐵] ∼ ∈ (𝑋 / ∼ )) |
9 | 8 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐵] ∼ ∈ (𝑋 / ∼ )) |
10 | | rexeq 3311 |
. . . . . 6
⊢ (𝑥 = [𝐴] ∼ →
(∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏))) |
11 | 10 | abbidv 2802 |
. . . . 5
⊢ (𝑥 = [𝐴] ∼ → {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
12 | 11 | unieqd 4810 |
. . . 4
⊢ (𝑥 = [𝐴] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
13 | | rexeq 3311 |
. . . . . . 7
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) |
14 | 13 | rexbidv 3207 |
. . . . . 6
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) |
15 | 14 | abbidv 2802 |
. . . . 5
⊢ (𝑦 = [𝐵] ∼ → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
16 | 15 | unieqd 4810 |
. . . 4
⊢ (𝑦 = [𝐵] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
17 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
18 | | ecexg 8326 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐴] ∼ ∈
V) |
19 | 5, 18 | ax-mp 5 |
. . . . . 6
⊢ [𝐴] ∼ ∈
V |
20 | | ecexg 8326 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐵] ∼ ∈
V) |
21 | 5, 20 | ax-mp 5 |
. . . . . 6
⊢ [𝐵] ∼ ∈
V |
22 | 19, 21 | ab2rexex 7707 |
. . . . 5
⊢ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V |
23 | 22 | uniex 7487 |
. . . 4
⊢ ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V |
24 | 12, 16, 17, 23 | ovmpo 7327 |
. . 3
⊢ (([𝐴] ∼ ∈ (𝑋 / ∼ ) ∧ [𝐵] ∼ ∈ (𝑋 / ∼ )) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
25 | 7, 9, 24 | syl2anc 587 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
26 | | simpr3 1197 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝑒𝐷𝑓)) |
27 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐷 ∈ (PsMet‘𝑋)) |
28 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑒 ∈ [𝐴] ∼ ) |
29 | | metidss 31415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (𝑋 × 𝑋)) |
30 | 1, 29 | eqsstrid 3925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (𝑋 × 𝑋)) |
31 | | xpss 5541 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
32 | 30, 31 | sstrdi 3889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (V ×
V)) |
33 | | df-rel 5532 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
∼
↔ ∼ ⊆ (V ×
V)) |
34 | 32, 33 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (PsMet‘𝑋) → Rel ∼ ) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Rel ∼ ) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → Rel ∼ ) |
37 | | relelec 8367 |
. . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) |
39 | 28, 38 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴 ∼ 𝑒) |
40 | 1 | breqi 5036 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∼ 𝑒 ↔ 𝐴(~Met‘𝐷)𝑒) |
41 | 39, 40 | sylib 221 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴(~Met‘𝐷)𝑒) |
42 | | simpr2 1196 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑓 ∈ [𝐵] ∼ ) |
43 | | relelec 8367 |
. . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) |
44 | 36, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) |
45 | 42, 44 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵 ∼ 𝑓) |
46 | 1 | breqi 5036 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∼ 𝑓 ↔ 𝐵(~Met‘𝐷)𝑓) |
47 | 45, 46 | sylib 221 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵(~Met‘𝐷)𝑓) |
48 | | metideq 31417 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝑒 ∧ 𝐵(~Met‘𝐷)𝑓)) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) |
49 | 27, 41, 47, 48 | syl12anc 836 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) |
50 | 26, 49 | eqtr4d 2776 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) |
51 | 50 | adantlr 715 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) |
52 | 51 | 3anassrs 1361 |
. . . . . . . 8
⊢
((((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ 𝑒 ∈ [𝐴] ∼ ) ∧ 𝑓 ∈ [𝐵] ∼ ) ∧ 𝑧 = (𝑒𝐷𝑓)) → 𝑧 = (𝐴𝐷𝐵)) |
53 | | oveq1 7179 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑒 → (𝑎𝐷𝑏) = (𝑒𝐷𝑏)) |
54 | 53 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑒 → (𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑏))) |
55 | | oveq2 7180 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑓 → (𝑒𝐷𝑏) = (𝑒𝐷𝑓)) |
56 | 55 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑓 → (𝑧 = (𝑒𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑓))) |
57 | 54, 56 | cbvrex2vw 3363 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
58 | 57 | biimpi 219 |
. . . . . . . . 9
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
59 | 58 | adantl 485 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
60 | 52, 59 | r19.29vva 3243 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → 𝑧 = (𝐴𝐷𝐵)) |
61 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐷 ∈ (PsMet‘𝑋)) |
62 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ 𝑋) |
63 | | psmet0 23063 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
64 | 61, 62, 63 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴𝐷𝐴) = 0) |
65 | | relelec 8367 |
. . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
66 | 61, 34, 65 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
67 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∼ =
(~Met‘𝐷)) |
68 | 67 | breqd 5041 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∼ 𝐴 ↔ 𝐴(~Met‘𝐷)𝐴)) |
69 | | metidv 31416 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) |
70 | 61, 62, 62, 69 | syl12anc 836 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) |
71 | 66, 68, 70 | 3bitrd 308 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ (𝐴𝐷𝐴) = 0)) |
72 | 64, 71 | mpbird 260 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ [𝐴] ∼ ) |
73 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ 𝑋) |
74 | | psmet0 23063 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵 ∈ 𝑋) → (𝐵𝐷𝐵) = 0) |
75 | 61, 73, 74 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵𝐷𝐵) = 0) |
76 | | relelec 8367 |
. . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) |
77 | 61, 34, 76 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) |
78 | 67 | breqd 5041 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∼ 𝐵 ↔ 𝐵(~Met‘𝐷)𝐵)) |
79 | | metidv 31416 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) |
80 | 61, 73, 73, 79 | syl12anc 836 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) |
81 | 77, 78, 80 | 3bitrd 308 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ (𝐵𝐷𝐵) = 0)) |
82 | 75, 81 | mpbird 260 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ [𝐵] ∼ ) |
83 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝑧 = (𝐴𝐷𝐵)) |
84 | | rspceov 7219 |
. . . . . . . 8
⊢ ((𝐴 ∈ [𝐴] ∼ ∧ 𝐵 ∈ [𝐵] ∼ ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) |
85 | 72, 82, 83, 84 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) |
86 | 60, 85 | impbida 801 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝐴𝐷𝐵))) |
87 | 86 | abbidv 2802 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)}) |
88 | | df-sn 4517 |
. . . . 5
⊢ {(𝐴𝐷𝐵)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)} |
89 | 87, 88 | eqtr4di 2791 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {(𝐴𝐷𝐵)}) |
90 | 89 | unieqd 4810 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = ∪ {(𝐴𝐷𝐵)}) |
91 | | ovex 7205 |
. . . 4
⊢ (𝐴𝐷𝐵) ∈ V |
92 | 91 | unisn 4818 |
. . 3
⊢ ∪ {(𝐴𝐷𝐵)} = (𝐴𝐷𝐵) |
93 | 90, 92 | eqtrdi 2789 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = (𝐴𝐷𝐵)) |
94 | 4, 25, 93 | 3eqtrd 2777 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) |