| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
| 2 | | xpeq12 5710 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑋 ∧ 𝑡 = 𝑋) → (𝑡 × 𝑡) = (𝑋 × 𝑋)) |
| 3 | 2 | anidms 566 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑋)) |
| 4 | 3 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (ℝ ↑m (𝑡 × 𝑡)) = (ℝ ↑m (𝑋 × 𝑋))) |
| 5 | | raleq 3323 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑋 → (∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)) ↔ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))) |
| 6 | 5 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → ((((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))) ↔ (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))))) |
| 7 | 6 | raleqbi1dv 3338 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (∀𝑦 ∈ 𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))) ↔ ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))))) |
| 8 | 7 | raleqbi1dv 3338 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))))) |
| 9 | 4, 8 | rabeqbidv 3455 |
. . . . . 6
⊢ (𝑡 = 𝑋 → {𝑑 ∈ (ℝ ↑m (𝑡 × 𝑡)) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))} = {𝑑 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))}) |
| 10 | | df-met 21358 |
. . . . . 6
⊢ Met =
(𝑡 ∈ V ↦ {𝑑 ∈ (ℝ
↑m (𝑡
× 𝑡)) ∣
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))}) |
| 11 | | ovex 7464 |
. . . . . . 7
⊢ (ℝ
↑m (𝑋
× 𝑋)) ∈
V |
| 12 | 11 | rabex 5339 |
. . . . . 6
⊢ {𝑑 ∈ (ℝ
↑m (𝑋
× 𝑋)) ∣
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))} ∈ V |
| 13 | 9, 10, 12 | fvmpt 7016 |
. . . . 5
⊢ (𝑋 ∈ V →
(Met‘𝑋) = {𝑑 ∈ (ℝ
↑m (𝑋
× 𝑋)) ∣
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))}) |
| 14 | 1, 13 | syl 17 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (Met‘𝑋) = {𝑑 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))}) |
| 15 | 14 | eleq2d 2827 |
. . 3
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ 𝐷 ∈ {𝑑 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))})) |
| 16 | | oveq 7437 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
| 17 | 16 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ((𝑥𝑑𝑦) = 0 ↔ (𝑥𝐷𝑦) = 0)) |
| 18 | 17 | bibi1d 343 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ↔ ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))) |
| 19 | | oveq 7437 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (𝑧𝑑𝑥) = (𝑧𝐷𝑥)) |
| 20 | | oveq 7437 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (𝑧𝑑𝑦) = (𝑧𝐷𝑦)) |
| 21 | 19, 20 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
| 22 | 16, 21 | breq12d 5156 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ((𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)) ↔ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))) |
| 23 | 22 | ralbidv 3178 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)) ↔ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))) |
| 24 | 18, 23 | anbi12d 632 |
. . . . 5
⊢ (𝑑 = 𝐷 → ((((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))) ↔ (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) |
| 25 | 24 | 2ralbidv 3221 |
. . . 4
⊢ (𝑑 = 𝐷 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) |
| 26 | 25 | elrab 3692 |
. . 3
⊢ (𝐷 ∈ {𝑑 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) + (𝑧𝑑𝑦)))} ↔ (𝐷 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) |
| 27 | 15, 26 | bitrdi 287 |
. 2
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) |
| 28 | | reex 11246 |
. . . 4
⊢ ℝ
∈ V |
| 29 | | sqxpexg 7775 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (𝑋 × 𝑋) ∈ V) |
| 30 | | elmapg 8879 |
. . . 4
⊢ ((ℝ
∈ V ∧ (𝑋 ×
𝑋) ∈ V) → (𝐷 ∈ (ℝ
↑m (𝑋
× 𝑋)) ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ)) |
| 31 | 28, 29, 30 | sylancr 587 |
. . 3
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (ℝ ↑m (𝑋 × 𝑋)) ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ)) |
| 32 | 31 | anbi1d 631 |
. 2
⊢ (𝑋 ∈ 𝐴 → ((𝐷 ∈ (ℝ ↑m (𝑋 × 𝑋)) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) |
| 33 | 27, 32 | bitrd 279 |
1
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) |