| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imasf1oxmet.u | . . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) | 
| 2 |  | imasf1oxmet.v | . . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) | 
| 3 |  | imasf1oxmet.f | . . . . 5
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) | 
| 4 |  | f1ofo 6854 | . . . . 5
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵) | 
| 5 | 3, 4 | syl 17 | . . . 4
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) | 
| 6 |  | imasf1oxmet.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑍) | 
| 7 |  | eqid 2736 | . . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) | 
| 8 |  | imasf1oxmet.d | . . . 4
⊢ 𝐷 = (dist‘𝑈) | 
| 9 | 1, 2, 5, 6, 7, 8 | imasdsfn 17560 | . . 3
⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) | 
| 10 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑈 = (𝐹 “s 𝑅)) | 
| 11 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑉 = (Base‘𝑅)) | 
| 12 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝐹:𝑉–1-1-onto→𝐵) | 
| 13 | 6 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑅 ∈ 𝑍) | 
| 14 |  | imasf1oxmet.e | . . . . . . . 8
⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) | 
| 15 |  | imasf1oxmet.m | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉)) | 
| 16 | 15 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝐸 ∈ (∞Met‘𝑉)) | 
| 17 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑎 ∈ 𝑉) | 
| 18 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑏 ∈ 𝑉) | 
| 19 | 10, 11, 12, 13, 14, 8, 16, 17, 18 | imasdsf1o 24385 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = (𝑎𝐸𝑏)) | 
| 20 |  | xmetcl 24342 | . . . . . . . . 9
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎𝐸𝑏) ∈
ℝ*) | 
| 21 | 20 | 3expb 1120 | . . . . . . . 8
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎𝐸𝑏) ∈
ℝ*) | 
| 22 | 15, 21 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎𝐸𝑏) ∈
ℝ*) | 
| 23 | 19, 22 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈
ℝ*) | 
| 24 | 23 | ralrimivva 3201 | . . . . 5
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈
ℝ*) | 
| 25 |  | f1ofn 6848 | . . . . . . . . 9
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹 Fn 𝑉) | 
| 26 | 3, 25 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑉) | 
| 27 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑏) → ((𝐹‘𝑎)𝐷𝑦) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) | 
| 28 | 27 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑏) → (((𝐹‘𝑎)𝐷𝑦) ∈ ℝ* ↔ ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈
ℝ*)) | 
| 29 | 28 | ralrn 7107 | . . . . . . . 8
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹((𝐹‘𝑎)𝐷𝑦) ∈ ℝ* ↔
∀𝑏 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈
ℝ*)) | 
| 30 | 26, 29 | syl 17 | . . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹((𝐹‘𝑎)𝐷𝑦) ∈ ℝ* ↔
∀𝑏 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈
ℝ*)) | 
| 31 |  | forn 6822 | . . . . . . . . 9
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) | 
| 32 | 5, 31 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ran 𝐹 = 𝐵) | 
| 33 | 32 | raleqdv 3325 | . . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹((𝐹‘𝑎)𝐷𝑦) ∈ ℝ* ↔
∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 34 | 30, 33 | bitr3d 281 | . . . . . 6
⊢ (𝜑 → (∀𝑏 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈ ℝ* ↔
∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 35 | 34 | ralbidv 3177 | . . . . 5
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ∈ ℝ* ↔
∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 36 | 24, 35 | mpbid 232 | . . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*) | 
| 37 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑎) → (𝑥𝐷𝑦) = ((𝐹‘𝑎)𝐷𝑦)) | 
| 38 | 37 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑎) → ((𝑥𝐷𝑦) ∈ ℝ* ↔ ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 39 | 38 | ralbidv 3177 | . . . . . . 7
⊢ (𝑥 = (𝐹‘𝑎) → (∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈ ℝ* ↔
∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 40 | 39 | ralrn 7107 | . . . . . 6
⊢ (𝐹 Fn 𝑉 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈ ℝ* ↔
∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 41 | 26, 40 | syl 17 | . . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈ ℝ* ↔
∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈
ℝ*)) | 
| 42 | 32 | raleqdv 3325 | . . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈ ℝ* ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈
ℝ*)) | 
| 43 | 41, 42 | bitr3d 281 | . . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ∈ ℝ* ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈
ℝ*)) | 
| 44 | 36, 43 | mpbid 232 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈
ℝ*) | 
| 45 |  | ffnov 7560 | . . 3
⊢ (𝐷:(𝐵 × 𝐵)⟶ℝ* ↔ (𝐷 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐷𝑦) ∈
ℝ*)) | 
| 46 | 9, 44, 45 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶ℝ*) | 
| 47 |  | xmeteq0 24349 | . . . . . . . 8
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑎𝐸𝑏) = 0 ↔ 𝑎 = 𝑏)) | 
| 48 | 16, 17, 18, 47 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑎𝐸𝑏) = 0 ↔ 𝑎 = 𝑏)) | 
| 49 | 19 | eqeq1d 2738 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝑎𝐸𝑏) = 0)) | 
| 50 |  | f1of1 6846 | . . . . . . . . 9
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵) | 
| 51 | 3, 50 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝑉–1-1→𝐵) | 
| 52 |  | f1fveq 7283 | . . . . . . . 8
⊢ ((𝐹:𝑉–1-1→𝐵 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ 𝑎 = 𝑏)) | 
| 53 | 51, 52 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ 𝑎 = 𝑏)) | 
| 54 | 48, 49, 53 | 3bitr4d 311 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) | 
| 55 | 16 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝐸 ∈ (∞Met‘𝑉)) | 
| 56 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) | 
| 57 | 17 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑎 ∈ 𝑉) | 
| 58 | 18 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑏 ∈ 𝑉) | 
| 59 |  | xmettri2 24351 | . . . . . . . . . 10
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎𝐸𝑏) ≤ ((𝑐𝐸𝑎) +𝑒 (𝑐𝐸𝑏))) | 
| 60 | 55, 56, 57, 58, 59 | syl13anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (𝑎𝐸𝑏) ≤ ((𝑐𝐸𝑎) +𝑒 (𝑐𝐸𝑏))) | 
| 61 | 19 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = (𝑎𝐸𝑏)) | 
| 62 | 10 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑈 = (𝐹 “s 𝑅)) | 
| 63 | 11 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑉 = (Base‘𝑅)) | 
| 64 | 12 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝐹:𝑉–1-1-onto→𝐵) | 
| 65 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → 𝑅 ∈ 𝑍) | 
| 66 | 62, 63, 64, 65, 14, 8, 55, 56, 57 | imasdsf1o 24385 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝐹‘𝑐)𝐷(𝐹‘𝑎)) = (𝑐𝐸𝑎)) | 
| 67 | 62, 63, 64, 65, 14, 8, 55, 56, 58 | imasdsf1o 24385 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝐹‘𝑐)𝐷(𝐹‘𝑏)) = (𝑐𝐸𝑏)) | 
| 68 | 66, 67 | oveq12d 7450 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))) = ((𝑐𝐸𝑎) +𝑒 (𝑐𝐸𝑏))) | 
| 69 | 60, 61, 68 | 3brtr4d 5174 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏)))) | 
| 70 | 69 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑐 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏)))) | 
| 71 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝐷(𝐹‘𝑎)) = ((𝐹‘𝑐)𝐷(𝐹‘𝑎))) | 
| 72 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝐷(𝐹‘𝑏)) = ((𝐹‘𝑐)𝐷(𝐹‘𝑏))) | 
| 73 | 71, 72 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))) = (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏)))) | 
| 74 | 73 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑐) → (((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))) ↔ ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))))) | 
| 75 | 74 | ralrn 7107 | . . . . . . . . . 10
⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))) ↔ ∀𝑐 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))))) | 
| 76 | 26, 75 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))) ↔ ∀𝑐 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))))) | 
| 77 | 32 | raleqdv 3325 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))) ↔ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 78 | 76, 77 | bitr3d 281 | . . . . . . . 8
⊢ (𝜑 → (∀𝑐 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))) ↔ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 79 | 78 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∀𝑐 ∈ 𝑉 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ (((𝐹‘𝑐)𝐷(𝐹‘𝑎)) +𝑒 ((𝐹‘𝑐)𝐷(𝐹‘𝑏))) ↔ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 80 | 70, 79 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))) | 
| 81 | 54, 80 | jca 511 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 82 | 81 | ralrimivva 3201 | . . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 83 | 27 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑏) → (((𝐹‘𝑎)𝐷𝑦) = 0 ↔ ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0)) | 
| 84 |  | eqeq2 2748 | . . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑏) → ((𝐹‘𝑎) = 𝑦 ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) | 
| 85 | 83, 84 | bibi12d 345 | . . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑏) → ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ↔ (((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)))) | 
| 86 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑏) → (𝑧𝐷𝑦) = (𝑧𝐷(𝐹‘𝑏))) | 
| 87 | 86 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑏) → ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))) | 
| 88 | 27, 87 | breq12d 5155 | . . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑏) → (((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)) ↔ ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 89 | 88 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑏) → (∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)) ↔ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏))))) | 
| 90 | 85, 89 | anbi12d 632 | . . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑏) → (((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) ↔ ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))))) | 
| 91 | 90 | ralrn 7107 | . . . . . . 7
⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑏 ∈ 𝑉 ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))))) | 
| 92 | 26, 91 | syl 17 | . . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑏 ∈ 𝑉 ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))))) | 
| 93 | 32 | raleqdv 3325 | . . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 94 | 92, 93 | bitr3d 281 | . . . . 5
⊢ (𝜑 → (∀𝑏 ∈ 𝑉 ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))) ↔ ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 95 | 94 | ralbidv 3177 | . . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ((((𝐹‘𝑎)𝐷(𝐹‘𝑏)) = 0 ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷(𝐹‘𝑏)) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷(𝐹‘𝑏)))) ↔ ∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 96 | 82, 95 | mpbid 232 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)))) | 
| 97 | 37 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑎) → ((𝑥𝐷𝑦) = 0 ↔ ((𝐹‘𝑎)𝐷𝑦) = 0)) | 
| 98 |  | eqeq1 2740 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑎) → (𝑥 = 𝑦 ↔ (𝐹‘𝑎) = 𝑦)) | 
| 99 | 97, 98 | bibi12d 345 | . . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑎) → (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ↔ (((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦))) | 
| 100 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐹‘𝑎) → (𝑧𝐷𝑥) = (𝑧𝐷(𝐹‘𝑎))) | 
| 101 | 100 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑎) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) | 
| 102 | 37, 101 | breq12d 5155 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑎) → ((𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) ↔ ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)))) | 
| 103 | 102 | ralbidv 3177 | . . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑎) → (∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) ↔ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦)))) | 
| 104 | 99, 103 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = (𝐹‘𝑎) → ((((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ↔ ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 105 | 104 | ralbidv 3177 | . . . . . 6
⊢ (𝑥 = (𝐹‘𝑎) → (∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 106 | 105 | ralrn 7107 | . . . . 5
⊢ (𝐹 Fn 𝑉 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 107 | 26, 106 | syl 17 | . . . 4
⊢ (𝜑 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))))) | 
| 108 | 32 | raleqdv 3325 | . . . 4
⊢ (𝜑 → (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))) | 
| 109 | 107, 108 | bitr3d 281 | . . 3
⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑦 ∈ 𝐵 ((((𝐹‘𝑎)𝐷𝑦) = 0 ↔ (𝐹‘𝑎) = 𝑦) ∧ ∀𝑧 ∈ 𝐵 ((𝐹‘𝑎)𝐷𝑦) ≤ ((𝑧𝐷(𝐹‘𝑎)) +𝑒 (𝑧𝐷𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))) | 
| 110 | 96, 109 | mpbid 232 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))) | 
| 111 | 15 | elfvexd 6944 | . . . 4
⊢ (𝜑 → 𝑉 ∈ V) | 
| 112 |  | focdmex 7981 | . . . 4
⊢ (𝑉 ∈ V → (𝐹:𝑉–onto→𝐵 → 𝐵 ∈ V)) | 
| 113 | 111, 5, 112 | sylc 65 | . . 3
⊢ (𝜑 → 𝐵 ∈ V) | 
| 114 |  | isxmet 24335 | . . 3
⊢ (𝐵 ∈ V → (𝐷 ∈ (∞Met‘𝐵) ↔ (𝐷:(𝐵 × 𝐵)⟶ℝ* ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | 
| 115 | 113, 114 | syl 17 | . 2
⊢ (𝜑 → (𝐷 ∈ (∞Met‘𝐵) ↔ (𝐷:(𝐵 × 𝐵)⟶ℝ* ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝐵 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | 
| 116 | 46, 110, 115 | mpbir2and 713 | 1
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) |