Step | Hyp | Ref
| Expression |
1 | | cvxpconn.4 |
. . 3
⊢ 𝐾 = (𝐽 ↾t 𝑆) |
2 | | cvxpconn.3 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
3 | 2 | cnfldtop 24687 |
. . . 4
⊢ 𝐽 ∈ Top |
4 | | cvxpconn.1 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | | cnex 11211 |
. . . . 5
⊢ ℂ
∈ V |
6 | | ssexg 5317 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
7 | 4, 5, 6 | sylancl 585 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ V) |
8 | | resttop 23051 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top) |
9 | 3, 7, 8 | sylancr 586 |
. . 3
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top) |
10 | 1, 9 | eqeltrid 2832 |
. 2
⊢ (𝜑 → 𝐾 ∈ Top) |
11 | 2 | dfii3 24790 |
. . . . . . . 8
⊢ II =
(𝐽 ↾t
(0[,]1)) |
12 | 2 | cnfldtopon 24686 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘ℂ) |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → 𝐽 ∈
(TopOn‘ℂ)) |
14 | | unitsscn 13501 |
. . . . . . . . 9
⊢ (0[,]1)
⊆ ℂ |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (0[,]1) ⊆
ℂ) |
16 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈
(TopOn‘ℂ)) |
17 | 16 | cnmptid 23552 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (𝐽 Cn 𝐽)) |
18 | 4 | sselda 3978 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ) |
19 | 16, 16, 18 | cnmptc 23553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑡 ∈ ℂ ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
20 | 2 | mpomulcn 24772 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
22 | | oveq12 7423 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑥) → (𝑢 · 𝑣) = (𝑡 · 𝑥)) |
23 | 16, 17, 19, 16, 16, 21, 22 | cnmpt12 23558 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑡 ∈ ℂ ↦ (𝑡 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
24 | 23 | adantrl 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ ℂ ↦ (𝑡 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
25 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈
(TopOn‘ℂ)) |
26 | | 1cnd 11231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
27 | 25, 25, 26 | cnmptc 23553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ 1) ∈ (𝐽 Cn 𝐽)) |
28 | 2 | cncfcn1 24818 |
. . . . . . . . . . . . . 14
⊢
(ℂ–cn→ℂ) =
(𝐽 Cn 𝐽) |
29 | 27, 28 | eleqtrrdi 2839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ 1) ∈
(ℂ–cn→ℂ)) |
30 | 25 | cnmptid 23552 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (𝐽 Cn 𝐽)) |
31 | 30, 28 | eleqtrrdi 2839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
32 | 29, 31 | subcncf 25360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (1 − 𝑡)) ∈ (ℂ–cn→ℂ)) |
33 | 32, 28 | eleqtrdi 2838 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (1 − 𝑡)) ∈ (𝐽 Cn 𝐽)) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ ℂ ↦ (1 − 𝑡)) ∈ (𝐽 Cn 𝐽)) |
35 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → 𝑆 ⊆ ℂ) |
36 | | simprl 770 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
37 | 35, 36 | sseldd 3979 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → 𝑦 ∈ ℂ) |
38 | 13, 13, 37 | cnmptc 23553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ ℂ ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) |
39 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
40 | | oveq12 7423 |
. . . . . . . . . 10
⊢ ((𝑢 = (1 − 𝑡) ∧ 𝑣 = 𝑦) → (𝑢 · 𝑣) = ((1 − 𝑡) · 𝑦)) |
41 | 13, 34, 38, 13, 13, 39, 40 | cnmpt12 23558 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ ℂ ↦ ((1 − 𝑡) · 𝑦)) ∈ (𝐽 Cn 𝐽)) |
42 | 2 | addcn 24768 |
. . . . . . . . . 10
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
43 | 42 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
44 | 13, 24, 41, 43 | cnmpt12f 23557 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ ℂ ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (𝐽 Cn 𝐽)) |
45 | 11, 13, 15, 44 | cnmpt1res 23567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn 𝐽)) |
46 | | cvxpconn.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) |
47 | 46 | 3exp2 1352 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑆 → (𝑦 ∈ 𝑆 → (𝑡 ∈ (0[,]1) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)))) |
48 | 47 | com23 86 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (𝑡 ∈ (0[,]1) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)))) |
49 | 48 | imp42 426 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) |
50 | 49 | fmpttd 7119 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))):(0[,]1)⟶𝑆) |
51 | 50 | frnd 6724 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ran (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ⊆ 𝑆) |
52 | | cnrest2 23177 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran (𝑡 ∈ (0[,]1)
↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ⊆ 𝑆 ∧ 𝑆 ⊆ ℂ) → ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn 𝐽) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn (𝐽 ↾t 𝑆)))) |
53 | 12, 51, 35, 52 | mp3an2i 1463 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn 𝐽) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn (𝐽 ↾t 𝑆)))) |
54 | 45, 53 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn (𝐽 ↾t 𝑆))) |
55 | 1 | oveq2i 7425 |
. . . . . 6
⊢ (II Cn
𝐾) = (II Cn (𝐽 ↾t 𝑆)) |
56 | 54, 55 | eleqtrrdi 2839 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn 𝐾)) |
57 | | 0elunit 13470 |
. . . . . . 7
⊢ 0 ∈
(0[,]1) |
58 | | oveq1 7421 |
. . . . . . . . 9
⊢ (𝑡 = 0 → (𝑡 · 𝑥) = (0 · 𝑥)) |
59 | | oveq2 7422 |
. . . . . . . . . . 11
⊢ (𝑡 = 0 → (1 − 𝑡) = (1 −
0)) |
60 | | 1m0e1 12355 |
. . . . . . . . . . 11
⊢ (1
− 0) = 1 |
61 | 59, 60 | eqtrdi 2783 |
. . . . . . . . . 10
⊢ (𝑡 = 0 → (1 − 𝑡) = 1) |
62 | 61 | oveq1d 7429 |
. . . . . . . . 9
⊢ (𝑡 = 0 → ((1 − 𝑡) · 𝑦) = (1 · 𝑦)) |
63 | 58, 62 | oveq12d 7432 |
. . . . . . . 8
⊢ (𝑡 = 0 → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((0 · 𝑥) + (1 · 𝑦))) |
64 | | eqid 2727 |
. . . . . . . 8
⊢ (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) |
65 | | ovex 7447 |
. . . . . . . 8
⊢ ((0
· 𝑥) + (1 ·
𝑦)) ∈
V |
66 | 63, 64, 65 | fvmpt 6999 |
. . . . . . 7
⊢ (0 ∈
(0[,]1) → ((𝑡 ∈
(0[,]1) ↦ ((𝑡
· 𝑥) + ((1 −
𝑡) · 𝑦)))‘0) = ((0 ·
𝑥) + (1 · 𝑦))) |
67 | 57, 66 | ax-mp 5 |
. . . . . 6
⊢ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0) = ((0 · 𝑥) + (1 · 𝑦)) |
68 | 18 | adantrl 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → 𝑥 ∈ ℂ) |
69 | 68 | mul02d 11434 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (0 · 𝑥) = 0) |
70 | 37 | mullidd 11254 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (1 · 𝑦) = 𝑦) |
71 | 69, 70 | oveq12d 7432 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((0 · 𝑥) + (1 · 𝑦)) = (0 + 𝑦)) |
72 | 37 | addlidd 11437 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (0 + 𝑦) = 𝑦) |
73 | 71, 72 | eqtrd 2767 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((0 · 𝑥) + (1 · 𝑦)) = 𝑦) |
74 | 67, 73 | eqtrid 2779 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0) = 𝑦) |
75 | | 1elunit 13471 |
. . . . . . 7
⊢ 1 ∈
(0[,]1) |
76 | | oveq1 7421 |
. . . . . . . . 9
⊢ (𝑡 = 1 → (𝑡 · 𝑥) = (1 · 𝑥)) |
77 | | oveq2 7422 |
. . . . . . . . . . 11
⊢ (𝑡 = 1 → (1 − 𝑡) = (1 −
1)) |
78 | | 1m1e0 12306 |
. . . . . . . . . . 11
⊢ (1
− 1) = 0 |
79 | 77, 78 | eqtrdi 2783 |
. . . . . . . . . 10
⊢ (𝑡 = 1 → (1 − 𝑡) = 0) |
80 | 79 | oveq1d 7429 |
. . . . . . . . 9
⊢ (𝑡 = 1 → ((1 − 𝑡) · 𝑦) = (0 · 𝑦)) |
81 | 76, 80 | oveq12d 7432 |
. . . . . . . 8
⊢ (𝑡 = 1 → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((1 · 𝑥) + (0 · 𝑦))) |
82 | | ovex 7447 |
. . . . . . . 8
⊢ ((1
· 𝑥) + (0 ·
𝑦)) ∈
V |
83 | 81, 64, 82 | fvmpt 6999 |
. . . . . . 7
⊢ (1 ∈
(0[,]1) → ((𝑡 ∈
(0[,]1) ↦ ((𝑡
· 𝑥) + ((1 −
𝑡) · 𝑦)))‘1) = ((1 ·
𝑥) + (0 · 𝑦))) |
84 | 75, 83 | ax-mp 5 |
. . . . . 6
⊢ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1) = ((1 · 𝑥) + (0 · 𝑦)) |
85 | 68 | mullidd 11254 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (1 · 𝑥) = 𝑥) |
86 | 37 | mul02d 11434 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (0 · 𝑦) = 0) |
87 | 85, 86 | oveq12d 7432 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((1 · 𝑥) + (0 · 𝑦)) = (𝑥 + 0)) |
88 | 68 | addridd 11436 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑥 + 0) = 𝑥) |
89 | 87, 88 | eqtrd 2767 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((1 · 𝑥) + (0 · 𝑦)) = 𝑥) |
90 | 84, 89 | eqtrid 2779 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1) = 𝑥) |
91 | | fveq1 6890 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (𝑓‘0) = ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0)) |
92 | 91 | eqeq1d 2729 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → ((𝑓‘0) = 𝑦 ↔ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0) = 𝑦)) |
93 | | fveq1 6890 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (𝑓‘1) = ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1)) |
94 | 93 | eqeq1d 2729 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → ((𝑓‘1) = 𝑥 ↔ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1) = 𝑥)) |
95 | 92, 94 | anbi12d 630 |
. . . . . 6
⊢ (𝑓 = (𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥) ↔ (((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0) = 𝑦 ∧ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1) = 𝑥))) |
96 | 95 | rspcev 3607 |
. . . . 5
⊢ (((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ (II Cn 𝐾) ∧ (((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘0) = 𝑦 ∧ ((𝑡 ∈ (0[,]1) ↦ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))‘1) = 𝑥)) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥)) |
97 | 56, 74, 90, 96 | syl12anc 836 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥)) |
98 | 97 | ralrimivva 3195 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ∀𝑥 ∈ 𝑆 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥)) |
99 | | resttopon 23052 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐽
↾t 𝑆)
∈ (TopOn‘𝑆)) |
100 | 12, 4, 99 | sylancr 586 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
101 | 1, 100 | eqeltrid 2832 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑆)) |
102 | | toponuni 22803 |
. . . . 5
⊢ (𝐾 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝐾) |
103 | 101, 102 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 = ∪ 𝐾) |
104 | 103 | raleqdv 3320 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑆 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥) ↔ ∀𝑥 ∈ ∪ 𝐾∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥))) |
105 | 103, 104 | raleqbidv 3337 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝑆 ∀𝑥 ∈ 𝑆 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥) ↔ ∀𝑦 ∈ ∪ 𝐾∀𝑥 ∈ ∪ 𝐾∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥))) |
106 | 98, 105 | mpbid 231 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ∪ 𝐾∀𝑥 ∈ ∪ 𝐾∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥)) |
107 | | eqid 2727 |
. . 3
⊢ ∪ 𝐾 =
∪ 𝐾 |
108 | 107 | ispconn 34769 |
. 2
⊢ (𝐾 ∈ PConn ↔ (𝐾 ∈ Top ∧ ∀𝑦 ∈ ∪ 𝐾∀𝑥 ∈ ∪ 𝐾∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑥))) |
109 | 10, 106, 108 | sylanbrc 582 |
1
⊢ (𝜑 → 𝐾 ∈ PConn) |