Step | Hyp | Ref
| Expression |
1 | | metucn.u |
. . . . . 6
⊢ 𝑈 = (metUnif‘𝐶) |
2 | | metucn.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋)) |
3 | | metuval 23315 |
. . . . . . 7
⊢ (𝐶 ∈ (PsMet‘𝑋) → (metUnif‘𝐶) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → (metUnif‘𝐶) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
5 | 1, 4 | syl5eq 2786 |
. . . . 5
⊢ (𝜑 → 𝑈 = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
6 | | metucn.v |
. . . . . 6
⊢ 𝑉 = (metUnif‘𝐷) |
7 | | metucn.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌)) |
8 | | metuval 23315 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑌) → (metUnif‘𝐷) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → (metUnif‘𝐷) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
10 | 6, 9 | syl5eq 2786 |
. . . . 5
⊢ (𝜑 → 𝑉 = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
11 | 5, 10 | oveq12d 7201 |
. . . 4
⊢ (𝜑 → (𝑈 Cnu𝑉) = (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))))) |
12 | 11 | eleq2d 2819 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ 𝐹 ∈ (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))))) |
13 | | eqid 2739 |
. . . 4
⊢ ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) |
14 | | eqid 2739 |
. . . 4
⊢ ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) |
15 | | metucn.x |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) |
16 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → (0[,)𝑎) = (0[,)𝑐)) |
17 | 16 | imaeq2d 5913 |
. . . . . . . 8
⊢ (𝑎 = 𝑐 → (◡𝐶 “ (0[,)𝑎)) = (◡𝐶 “ (0[,)𝑐))) |
18 | 17 | cbvmptv 5143 |
. . . . . . 7
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) = (𝑐 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑐))) |
19 | 18 | rneqi 5790 |
. . . . . 6
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) = ran (𝑐 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑐))) |
20 | 19 | metust 23324 |
. . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝐶 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) ∈ (UnifOn‘𝑋)) |
21 | 15, 2, 20 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) ∈ (UnifOn‘𝑋)) |
22 | | metucn.y |
. . . . 5
⊢ (𝜑 → 𝑌 ≠ ∅) |
23 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (0[,)𝑏) = (0[,)𝑑)) |
24 | 23 | imaeq2d 5913 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)𝑑))) |
25 | 24 | cbvmptv 5143 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) = (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) |
26 | 25 | rneqi 5790 |
. . . . . 6
⊢ ran
(𝑏 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) = ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) |
27 | 26 | metust 23324 |
. . . . 5
⊢ ((𝑌 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑌)) → ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) ∈ (UnifOn‘𝑌)) |
28 | 22, 7, 27 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) ∈ (UnifOn‘𝑌)) |
29 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (0[,)𝑎) = (0[,)𝑒)) |
30 | 29 | imaeq2d 5913 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (◡𝐶 “ (0[,)𝑎)) = (◡𝐶 “ (0[,)𝑒))) |
31 | 30 | cbvmptv 5143 |
. . . . . . 7
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) = (𝑒 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑒))) |
32 | 31 | rneqi 5790 |
. . . . . 6
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) = ran (𝑒 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑒))) |
33 | 32 | metustfbas 23323 |
. . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝐶 ∈ (PsMet‘𝑋)) → ran (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) ∈ (fBas‘(𝑋 × 𝑋))) |
34 | 15, 2, 33 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ∈ (fBas‘(𝑋 × 𝑋))) |
35 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑏 = 𝑓 → (0[,)𝑏) = (0[,)𝑓)) |
36 | 35 | imaeq2d 5913 |
. . . . . . . 8
⊢ (𝑏 = 𝑓 → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)𝑓))) |
37 | 36 | cbvmptv 5143 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) = (𝑓 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑓))) |
38 | 37 | rneqi 5790 |
. . . . . 6
⊢ ran
(𝑏 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) = ran (𝑓 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑓))) |
39 | 38 | metustfbas 23323 |
. . . . 5
⊢ ((𝑌 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑌)) → ran (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) ∈ (fBas‘(𝑌 × 𝑌))) |
40 | 22, 7, 39 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ∈ (fBas‘(𝑌 × 𝑌))) |
41 | 13, 14, 21, 28, 34, 40 | isucn2 23044 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
42 | 12, 41 | bitrd 282 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
43 | | eqid 2739 |
. . . . . . . . . 10
⊢ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑑)) |
44 | | oveq2 7191 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑑 → (0[,)𝑓) = (0[,)𝑑)) |
45 | 44 | imaeq2d 5913 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑑 → (◡𝐷 “ (0[,)𝑓)) = (◡𝐷 “ (0[,)𝑑))) |
46 | 45 | rspceeqv 3544 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℝ+
∧ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑑))) → ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
47 | 43, 46 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ+
→ ∃𝑓 ∈
ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
48 | 47 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) →
∃𝑓 ∈
ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
49 | 38 | metustel 23316 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑌) → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
50 | 7, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
52 | 48, 51 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) |
53 | 26 | metustel 23316 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑌) → (𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑑 ∈ ℝ+ 𝑣 = (◡𝐷 “ (0[,)𝑑)))) |
54 | 7, 53 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑑 ∈ ℝ+ 𝑣 = (◡𝐷 “ (0[,)𝑑)))) |
55 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → 𝑣 = (◡𝐷 “ (0[,)𝑑))) |
56 | 55 | breqd 5051 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → ((𝐹‘𝑥)𝑣(𝐹‘𝑦) ↔ (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦))) |
57 | 56 | imbi2d 344 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
58 | 57 | ralbidv 3110 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
59 | 58 | rexralbidv 3212 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → (∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
60 | 52, 54, 59 | ralxfr2d 5287 |
. . . . . 6
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
61 | | eqid 2739 |
. . . . . . . . . . 11
⊢ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑐)) |
62 | | oveq2 7191 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑐 → (0[,)𝑒) = (0[,)𝑐)) |
63 | 62 | imaeq2d 5913 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑐 → (◡𝐶 “ (0[,)𝑒)) = (◡𝐶 “ (0[,)𝑐))) |
64 | 63 | rspceeqv 3544 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℝ+
∧ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑐))) → ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
65 | 61, 64 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℝ+
→ ∃𝑒 ∈
ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
66 | 65 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) →
∃𝑒 ∈
ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
67 | 32 | metustel 23316 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (PsMet‘𝑋) → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
68 | 2, 67 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
69 | 68 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
70 | 66, 69 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) → (◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) |
71 | 19 | metustel 23316 |
. . . . . . . . 9
⊢ (𝐶 ∈ (PsMet‘𝑋) → (𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑐 ∈ ℝ+ 𝑢 = (◡𝐶 “ (0[,)𝑐)))) |
72 | 2, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑐 ∈ ℝ+ 𝑢 = (◡𝐶 “ (0[,)𝑐)))) |
73 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → 𝑢 = (◡𝐶 “ (0[,)𝑐))) |
74 | 73 | breqd 5051 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → (𝑥𝑢𝑦 ↔ 𝑥(◡𝐶 “ (0[,)𝑐))𝑦)) |
75 | 74 | imbi1d 345 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
76 | 75 | 2ralbidv 3112 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
77 | 70, 72, 76 | rexxfr2d 5288 |
. . . . . . 7
⊢ (𝜑 → (∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
78 | 77 | ralbidv 3110 |
. . . . . 6
⊢ (𝜑 → (∀𝑑 ∈ ℝ+
∃𝑢 ∈ ran (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
79 | 60, 78 | bitrd 282 |
. . . . 5
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
80 | 79 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
81 | 2 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐶 ∈ (PsMet‘𝑋)) |
82 | | simplr 769 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ ℝ+) |
83 | | simprr 773 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
84 | | simprl 771 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
85 | | elbl4 23329 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ 𝑥(◡𝐶 “ (0[,)𝑐))𝑦)) |
86 | | rpxr 12494 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
87 | | elbl3ps 23157 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ (𝑥𝐶𝑦) < 𝑐)) |
88 | 86, 87 | sylanl2 681 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ (𝑥𝐶𝑦) < 𝑐)) |
89 | 85, 88 | bitr3d 284 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 ↔ (𝑥𝐶𝑦) < 𝑐)) |
90 | 81, 82, 83, 84, 89 | syl22anc 838 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 ↔ (𝑥𝐶𝑦) < 𝑐)) |
91 | 7 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐷 ∈ (PsMet‘𝑌)) |
92 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ ℝ+) |
93 | | simp-4r 784 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐹:𝑋⟶𝑌) |
94 | 93, 83 | ffvelrnd 6875 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ 𝑌) |
95 | 93, 84 | ffvelrnd 6875 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝑥) ∈ 𝑌) |
96 | | elbl4 23329 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦))) |
97 | | rpxr 12494 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ*) |
98 | | elbl3ps 23157 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ*) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
99 | 97, 98 | sylanl2 681 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
100 | 96, 99 | bitr3d 284 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
101 | 91, 92, 94, 95, 100 | syl22anc 838 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
102 | 90, 101 | imbi12d 348 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
103 | 102 | 2ralbidva 3111 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
→ (∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
104 | 103 | rexbidva 3207 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) →
(∃𝑐 ∈
ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
105 | 104 | ralbidva 3109 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
106 | 80, 105 | bitrd 282 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
107 | 106 | pm5.32da 582 |
. 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) |
108 | 42, 107 | bitrd 282 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) |