Step | Hyp | Ref
| Expression |
1 | | pstmval.1 |
. . . . 5
⊢ ∼ =
(~Met‘𝐷) |
2 | 1 | pstmval 29938 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) |
3 | 2 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (pstoMet‘𝐷) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})) |
4 | 3 | oveqd 6667 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ )) |
5 | | fvex 6201 |
. . . . . 6
⊢
(~Met‘𝐷) ∈ V |
6 | 1, 5 | eqeltri 2697 |
. . . . 5
⊢ ∼ ∈
V |
7 | 6 | ecelqsi 7803 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ ∈ (𝑋 / ∼ )) |
8 | 7 | 3ad2ant2 1083 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐴] ∼ ∈ (𝑋 / ∼ )) |
9 | 6 | ecelqsi 7803 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → [𝐵] ∼ ∈ (𝑋 / ∼ )) |
10 | 9 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → [𝐵] ∼ ∈ (𝑋 / ∼ )) |
11 | | rexeq 3139 |
. . . . . 6
⊢ (𝑥 = [𝐴] ∼ →
(∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏))) |
12 | 11 | abbidv 2741 |
. . . . 5
⊢ (𝑥 = [𝐴] ∼ → {𝑧 ∣ ∃𝑎 ∈ 𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
13 | 12 | unieqd 4446 |
. . . 4
⊢ (𝑥 = [𝐴] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
14 | | rexeq 3139 |
. . . . . . 7
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) |
15 | 14 | rexbidv 3052 |
. . . . . 6
⊢ (𝑦 = [𝐵] ∼ →
(∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏))) |
16 | 15 | abbidv 2741 |
. . . . 5
⊢ (𝑦 = [𝐵] ∼ → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
17 | 16 | unieqd 4446 |
. . . 4
⊢ (𝑦 = [𝐵] ∼ → ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)} = ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
18 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) = (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)}) |
19 | | ecexg 7746 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐴] ∼ ∈
V) |
20 | 6, 19 | ax-mp 5 |
. . . . . 6
⊢ [𝐴] ∼ ∈
V |
21 | | ecexg 7746 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐵] ∼ ∈
V) |
22 | 6, 21 | ax-mp 5 |
. . . . . 6
⊢ [𝐵] ∼ ∈
V |
23 | 20, 22 | ab2rexex 7159 |
. . . . 5
⊢ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V |
24 | 23 | uniex 6953 |
. . . 4
⊢ ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} ∈ V |
25 | 13, 17, 18, 24 | ovmpt2 6796 |
. . 3
⊢ (([𝐴] ∼ ∈ (𝑋 / ∼ ) ∧ [𝐵] ∼ ∈ (𝑋 / ∼ )) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
26 | 8, 10, 25 | syl2anc 693 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (𝑥 ∈ (𝑋 / ∼ ), 𝑦 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧
∣ ∃𝑎 ∈
𝑥 ∃𝑏 ∈ 𝑦 𝑧 = (𝑎𝐷𝑏)})[𝐵] ∼ ) = ∪ {𝑧
∣ ∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)}) |
27 | | simpr3 1069 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝑒𝐷𝑓)) |
28 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐷 ∈ (PsMet‘𝑋)) |
29 | | simpr1 1067 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑒 ∈ [𝐴] ∼ ) |
30 | | metidss 29934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (𝑋 × 𝑋)) |
31 | 1, 30 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (𝑋 × 𝑋)) |
32 | | xpss 5226 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
33 | 31, 32 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∼ ⊆ (V ×
V)) |
34 | | df-rel 5121 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
∼
↔ ∼ ⊆ (V ×
V)) |
35 | 33, 34 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (PsMet‘𝑋) → Rel ∼ ) |
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Rel ∼ ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → Rel ∼ ) |
38 | | relelec 7787 |
. . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑒 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑒)) |
40 | 29, 39 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴 ∼ 𝑒) |
41 | 1 | breqi 4659 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∼ 𝑒 ↔ 𝐴(~Met‘𝐷)𝑒) |
42 | 40, 41 | sylib 208 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐴(~Met‘𝐷)𝑒) |
43 | | simpr2 1068 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑓 ∈ [𝐵] ∼ ) |
44 | | relelec 7787 |
. . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) |
45 | 37, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝑓 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝑓)) |
46 | 43, 45 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵 ∼ 𝑓) |
47 | 1 | breqi 4659 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∼ 𝑓 ↔ 𝐵(~Met‘𝐷)𝑓) |
48 | 46, 47 | sylib 208 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝐵(~Met‘𝐷)𝑓) |
49 | | metideq 29936 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝑒 ∧ 𝐵(~Met‘𝐷)𝑓)) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) |
50 | 28, 42, 48, 49 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → (𝐴𝐷𝐵) = (𝑒𝐷𝑓)) |
51 | 27, 50 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) |
52 | 51 | adantlr 751 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ (𝑒 ∈ [𝐴] ∼ ∧ 𝑓 ∈ [𝐵] ∼ ∧ 𝑧 = (𝑒𝐷𝑓))) → 𝑧 = (𝐴𝐷𝐵)) |
53 | 52 | 3anassrs 1290 |
. . . . . . . 8
⊢
((((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) ∧ 𝑒 ∈ [𝐴] ∼ ) ∧ 𝑓 ∈ [𝐵] ∼ ) ∧ 𝑧 = (𝑒𝐷𝑓)) → 𝑧 = (𝐴𝐷𝐵)) |
54 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑒 → (𝑎𝐷𝑏) = (𝑒𝐷𝑏)) |
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑒 → (𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑏))) |
56 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑓 → (𝑒𝐷𝑏) = (𝑒𝐷𝑓)) |
57 | 56 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑓 → (𝑧 = (𝑒𝐷𝑏) ↔ 𝑧 = (𝑒𝐷𝑓))) |
58 | 55, 57 | cbvrex2v 3180 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
59 | 58 | biimpi 206 |
. . . . . . . . 9
⊢
(∃𝑎 ∈ [
𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
60 | 59 | adantl 482 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → ∃𝑒 ∈ [ 𝐴] ∼ ∃𝑓 ∈ [ 𝐵] ∼ 𝑧 = (𝑒𝐷𝑓)) |
61 | 53, 60 | r19.29vva 3081 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) → 𝑧 = (𝐴𝐷𝐵)) |
62 | | simpl1 1064 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐷 ∈ (PsMet‘𝑋)) |
63 | | simpl2 1065 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ 𝑋) |
64 | | psmet0 22113 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
65 | 62, 63, 64 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴𝐷𝐴) = 0) |
66 | | relelec 7787 |
. . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
67 | 62, 35, 66 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
68 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∼ =
(~Met‘𝐷)) |
69 | 68 | breqd 4664 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∼ 𝐴 ↔ 𝐴(~Met‘𝐷)𝐴)) |
70 | | metidv 29935 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) |
71 | 62, 63, 63, 70 | syl12anc 1324 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴(~Met‘𝐷)𝐴 ↔ (𝐴𝐷𝐴) = 0)) |
72 | 67, 69, 71 | 3bitrd 294 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐴 ∈ [𝐴] ∼ ↔ (𝐴𝐷𝐴) = 0)) |
73 | 65, 72 | mpbird 247 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐴 ∈ [𝐴] ∼ ) |
74 | | simpl3 1066 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ 𝑋) |
75 | | psmet0 22113 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵 ∈ 𝑋) → (𝐵𝐷𝐵) = 0) |
76 | 62, 74, 75 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵𝐷𝐵) = 0) |
77 | | relelec 7787 |
. . . . . . . . . . 11
⊢ (Rel
∼
→ (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) |
78 | 62, 35, 77 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ 𝐵 ∼ 𝐵)) |
79 | 68 | breqd 4664 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∼ 𝐵 ↔ 𝐵(~Met‘𝐷)𝐵)) |
80 | | metidv 29935 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) |
81 | 62, 74, 74, 80 | syl12anc 1324 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵(~Met‘𝐷)𝐵 ↔ (𝐵𝐷𝐵) = 0)) |
82 | 78, 79, 81 | 3bitrd 294 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → (𝐵 ∈ [𝐵] ∼ ↔ (𝐵𝐷𝐵) = 0)) |
83 | 76, 82 | mpbird 247 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝐵 ∈ [𝐵] ∼ ) |
84 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → 𝑧 = (𝐴𝐷𝐵)) |
85 | | rspceov 6692 |
. . . . . . . 8
⊢ ((𝐴 ∈ [𝐴] ∼ ∧ 𝐵 ∈ [𝐵] ∼ ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) |
86 | 73, 83, 84, 85 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑧 = (𝐴𝐷𝐵)) → ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)) |
87 | 61, 86 | impbida 877 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏) ↔ 𝑧 = (𝐴𝐷𝐵))) |
88 | 87 | abbidv 2741 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)}) |
89 | | df-sn 4178 |
. . . . 5
⊢ {(𝐴𝐷𝐵)} = {𝑧 ∣ 𝑧 = (𝐴𝐷𝐵)} |
90 | 88, 89 | syl6eqr 2674 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = {(𝐴𝐷𝐵)}) |
91 | 90 | unieqd 4446 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = ∪ {(𝐴𝐷𝐵)}) |
92 | | ovex 6678 |
. . . 4
⊢ (𝐴𝐷𝐵) ∈ V |
93 | 92 | unisn 4451 |
. . 3
⊢ ∪ {(𝐴𝐷𝐵)} = (𝐴𝐷𝐵) |
94 | 91, 93 | syl6eq 2672 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∪ {𝑧 ∣ ∃𝑎 ∈ [ 𝐴] ∼ ∃𝑏 ∈ [ 𝐵] ∼ 𝑧 = (𝑎𝐷𝑏)} = (𝐴𝐷𝐵)) |
95 | 4, 26, 94 | 3eqtrd 2660 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼
(pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) |