Step | Hyp | Ref
| Expression |
1 | | metucn.u |
. . . . . 6
⊢ 𝑈 = (metUnif‘𝐶) |
2 | | metucn.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋)) |
3 | | metuval 22354 |
. . . . . . 7
⊢ (𝐶 ∈ (PsMet‘𝑋) → (metUnif‘𝐶) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → (metUnif‘𝐶) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
5 | 1, 4 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → 𝑈 = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))))) |
6 | | metucn.v |
. . . . . 6
⊢ 𝑉 = (metUnif‘𝐷) |
7 | | metucn.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌)) |
8 | | metuval 22354 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑌) → (metUnif‘𝐷) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → (metUnif‘𝐷) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
10 | 6, 9 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → 𝑉 = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) |
11 | 5, 10 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (𝑈 Cnu𝑉) = (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))))) |
12 | 11 | eleq2d 2687 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ 𝐹 ∈ (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))))) |
13 | | eqid 2622 |
. . . 4
⊢ ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) |
14 | | eqid 2622 |
. . . 4
⊢ ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) = ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) |
15 | | metucn.x |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) |
16 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → (0[,)𝑎) = (0[,)𝑐)) |
17 | 16 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑎 = 𝑐 → (◡𝐶 “ (0[,)𝑎)) = (◡𝐶 “ (0[,)𝑐))) |
18 | 17 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) = (𝑐 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑐))) |
19 | 18 | rneqi 5352 |
. . . . . 6
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) = ran (𝑐 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑐))) |
20 | 19 | metust 22363 |
. . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝐶 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) ∈ (UnifOn‘𝑋)) |
21 | 15, 2, 20 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) ∈ (UnifOn‘𝑋)) |
22 | | metucn.y |
. . . . 5
⊢ (𝜑 → 𝑌 ≠ ∅) |
23 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (0[,)𝑏) = (0[,)𝑑)) |
24 | 23 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)𝑑))) |
25 | 24 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) = (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) |
26 | 25 | rneqi 5352 |
. . . . . 6
⊢ ran
(𝑏 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) = ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) |
27 | 26 | metust 22363 |
. . . . 5
⊢ ((𝑌 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑌)) → ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) ∈ (UnifOn‘𝑌)) |
28 | 22, 7, 27 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) ∈ (UnifOn‘𝑌)) |
29 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (0[,)𝑎) = (0[,)𝑒)) |
30 | 29 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (◡𝐶 “ (0[,)𝑎)) = (◡𝐶 “ (0[,)𝑒))) |
31 | 30 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) = (𝑒 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑒))) |
32 | 31 | rneqi 5352 |
. . . . . 6
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) = ran (𝑒 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑒))) |
33 | 32 | metustfbas 22362 |
. . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝐶 ∈ (PsMet‘𝑋)) → ran (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎))) ∈ (fBas‘(𝑋 × 𝑋))) |
34 | 15, 2, 33 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ∈ (fBas‘(𝑋 × 𝑋))) |
35 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑏 = 𝑓 → (0[,)𝑏) = (0[,)𝑓)) |
36 | 35 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑏 = 𝑓 → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)𝑓))) |
37 | 36 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) = (𝑓 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑓))) |
38 | 37 | rneqi 5352 |
. . . . . 6
⊢ ran
(𝑏 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) = ran (𝑓 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑓))) |
39 | 38 | metustfbas 22362 |
. . . . 5
⊢ ((𝑌 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑌)) → ran (𝑏 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑏))) ∈ (fBas‘(𝑌 × 𝑌))) |
40 | 22, 7, 39 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ∈ (fBas‘(𝑌 × 𝑌))) |
41 | 13, 14, 21, 28, 34, 40 | isucn2 22083 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) Cnu((𝑌 × 𝑌)filGenran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
42 | 12, 41 | bitrd 268 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
43 | | eqid 2622 |
. . . . . . . . . 10
⊢ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑑)) |
44 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑑 → (0[,)𝑓) = (0[,)𝑑)) |
45 | 44 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑑 → (◡𝐷 “ (0[,)𝑓)) = (◡𝐷 “ (0[,)𝑑))) |
46 | 45 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑑 → ((◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)) ↔ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑑)))) |
47 | 46 | rspcev 3309 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℝ+
∧ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑑))) → ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
48 | 43, 47 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ+
→ ∃𝑓 ∈
ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
49 | 48 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) →
∃𝑓 ∈
ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓))) |
50 | 38 | metustel 22355 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑌) → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
51 | 7, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
52 | 51 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) → ((◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑓 ∈ ℝ+ (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑓)))) |
53 | 49, 52 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑑)) ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))) |
54 | 26 | metustel 22355 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑌) → (𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑑 ∈ ℝ+ 𝑣 = (◡𝐷 “ (0[,)𝑑)))) |
55 | 7, 54 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) ↔ ∃𝑑 ∈ ℝ+ 𝑣 = (◡𝐷 “ (0[,)𝑑)))) |
56 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → 𝑣 = (◡𝐷 “ (0[,)𝑑))) |
57 | 56 | breqd 4664 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → ((𝐹‘𝑥)𝑣(𝐹‘𝑦) ↔ (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦))) |
58 | 57 | imbi2d 330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
59 | 58 | ralbidv 2986 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → (∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
60 | 59 | rexralbidv 3058 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 = (◡𝐷 “ (0[,)𝑑))) → (∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
61 | 53, 55, 60 | ralxfr2d 4882 |
. . . . . 6
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
62 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑐)) |
63 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = 𝑐 → (0[,)𝑒) = (0[,)𝑐)) |
64 | 63 | imaeq2d 5466 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝑐 → (◡𝐶 “ (0[,)𝑒)) = (◡𝐶 “ (0[,)𝑐))) |
65 | 64 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑐 → ((◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)) ↔ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑐)))) |
66 | 65 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℝ+
∧ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑐))) → ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
67 | 62, 66 | mpan2 707 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℝ+
→ ∃𝑒 ∈
ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
68 | 67 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) →
∃𝑒 ∈
ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒))) |
69 | 32 | metustel 22355 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (PsMet‘𝑋) → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
70 | 2, 69 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
71 | 70 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) → ((◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑒 ∈ ℝ+ (◡𝐶 “ (0[,)𝑐)) = (◡𝐶 “ (0[,)𝑒)))) |
72 | 68, 71 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+) → (◡𝐶 “ (0[,)𝑐)) ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))) |
73 | 19 | metustel 22355 |
. . . . . . . . 9
⊢ (𝐶 ∈ (PsMet‘𝑋) → (𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑐 ∈ ℝ+ 𝑢 = (◡𝐶 “ (0[,)𝑐)))) |
74 | 2, 73 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎))) ↔ ∃𝑐 ∈ ℝ+ 𝑢 = (◡𝐶 “ (0[,)𝑐)))) |
75 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → 𝑢 = (◡𝐶 “ (0[,)𝑐))) |
76 | 75 | breqd 4664 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → (𝑥𝑢𝑦 ↔ 𝑥(◡𝐶 “ (0[,)𝑐))𝑦)) |
77 | 76 | imbi1d 331 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → ((𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
78 | 77 | 2ralbidv 2989 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 = (◡𝐶 “ (0[,)𝑐))) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
79 | 72, 74, 78 | rexxfr2d 4883 |
. . . . . . 7
⊢ (𝜑 → (∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
80 | 79 | ralbidv 2986 |
. . . . . 6
⊢ (𝜑 → (∀𝑑 ∈ ℝ+
∃𝑢 ∈ ran (𝑎 ∈ ℝ+
↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
81 | 61, 80 | bitrd 268 |
. . . . 5
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
82 | 81 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)))) |
83 | 2 | ad4antr 768 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐶 ∈ (PsMet‘𝑋)) |
84 | | simplr 792 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ ℝ+) |
85 | | simprr 796 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
86 | | simprl 794 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
87 | | elbl4 22368 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ 𝑥(◡𝐶 “ (0[,)𝑐))𝑦)) |
88 | | rpxr 11840 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
89 | | elbl3ps 22196 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ (𝑥𝐶𝑦) < 𝑐)) |
90 | 88, 89 | sylanl2 683 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝐶)𝑐) ↔ (𝑥𝐶𝑦) < 𝑐)) |
91 | 87, 90 | bitr3d 270 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (PsMet‘𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 ↔ (𝑥𝐶𝑦) < 𝑐)) |
92 | 83, 84, 85, 86, 91 | syl22anc 1327 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 ↔ (𝑥𝐶𝑦) < 𝑐)) |
93 | 7 | ad4antr 768 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐷 ∈ (PsMet‘𝑌)) |
94 | | simpllr 799 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ ℝ+) |
95 | | simp-4r 807 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐹:𝑋⟶𝑌) |
96 | 95, 85 | ffvelrnd 6360 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ 𝑌) |
97 | 95, 86 | ffvelrnd 6360 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝑥) ∈ 𝑌) |
98 | | elbl4 22368 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦))) |
99 | | rpxr 11840 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ*) |
100 | | elbl3ps 22196 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ*) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
101 | 99, 100 | sylanl2 683 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥) ∈ ((𝐹‘𝑦)(ball‘𝐷)𝑑) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
102 | 98, 101 | bitr3d 270 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ((𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑥) ∈ 𝑌)) → ((𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
103 | 93, 94, 96, 97, 102 | syl22anc 1327 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦) ↔ ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)) |
104 | 92, 103 | imbi12d 334 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
105 | 104 | 2ralbidva 2988 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑐 ∈ ℝ+)
→ (∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
106 | 105 | rexbidva 3049 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑑 ∈ ℝ+) →
(∃𝑐 ∈
ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
107 | 106 | ralbidva 2985 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(◡𝐶 “ (0[,)𝑐))𝑦 → (𝐹‘𝑥)(◡𝐷 “ (0[,)𝑑))(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
108 | 82, 107 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))) |
109 | 108 | pm5.32da 673 |
. 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))∃𝑢 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐶 “ (0[,)𝑎)))∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑢𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) |
110 | 42, 109 | bitrd 268 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) |