Metamath Proof Explorer

Theorem cvxpconn

Description: A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

Ref Expression
Hypotheses cvxpconn.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
cvxpconn.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
cvxpconn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cvxpconn.4 ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
Assertion cvxpconn ( 𝜑 → 𝐾 ∈ PConn )

Proof

Step Hyp Ref Expression
1 cvxpconn.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 cvxpconn.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
3 cvxpconn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
4 cvxpconn.4 ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
5 3 cnfldtop ⊢ 𝐽 ∈ Top
6 cnex ⊢ ℂ ∈ V
7 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
8 1 6 7 sylancl ⊢ ( 𝜑 → 𝑆 ∈ V )
9 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐽 ↾t 𝑆 ) ∈ Top )
10 5 8 9 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ Top )
11 4 10 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ Top )
12 3 dfii3 ⊢ II = ( 𝐽 ↾t ( 0 [,] 1 ) )
13 3 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
14 13 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
15 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
16 15 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 [,] 1 ) ⊆ ℂ )
17 13 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
18 17 cnmptid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( 𝐽 Cn 𝐽 ) )
19 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℂ )
20 17 17 19 cnmptc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑡 ∈ ℂ ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
21 3 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
23 oveq12 ⊢ ( ( 𝑢 = 𝑡 ∧ 𝑣 = 𝑥 ) → ( 𝑢 · 𝑣 ) = ( 𝑡 · 𝑥 ) )
24 17 18 20 17 17 22 23 cnmpt12 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
25 24 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
26 13 a1i ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ℂ ) )
27 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
28 26 26 27 cnmptc ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ 1 ) ∈ ( 𝐽 Cn 𝐽 ) )
29 3 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )
30 28 29 eleqtrrdi ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ 1 ) ∈ ( ℂ –cn→ ℂ ) )
31 26 cnmptid ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( 𝐽 Cn 𝐽 ) )
32 31 29 eleqtrrdi ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ ) )
33 30 32 subcncf ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 1 − 𝑡 ) ) ∈ ( ℂ –cn→ ℂ ) )
34 33 29 eleqtrdi ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 1 − 𝑡 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( 1 − 𝑡 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
36 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑆 ⊆ ℂ )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
38 36 37 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑦 ∈ ℂ )
39 14 14 38 cnmptc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
40 21 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
41 oveq12 ⊢ ( ( 𝑢 = ( 1 − 𝑡 ) ∧ 𝑣 = 𝑦 ) → ( 𝑢 · 𝑣 ) = ( ( 1 − 𝑡 ) · 𝑦 ) )
42 14 35 39 14 14 40 41 cnmpt12 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
43 3 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
44 43 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
45 14 25 42 44 cnmpt12f ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
46 12 14 16 45 cnmpt1res ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) )
47 2 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → ( 𝑦 ∈ 𝑆 → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) ) ) )
48 47 com23 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) ) ) )
49 48 imp42 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
50 49 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) : ( 0 [,] 1 ) ⟶ 𝑆 )
51 50 frnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ran ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ⊆ 𝑆 )
52 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ⊆ 𝑆 ∧ 𝑆 ⊆ ℂ ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) ) )
53 13 51 36 52 mp3an2i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) ) )
54 46 53 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) )
55 4 oveq2i ⊢ ( II Cn 𝐾 ) = ( II Cn ( 𝐽 ↾t 𝑆 ) )
56 54 55 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐾 ) )
57 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
58 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 · 𝑥 ) = ( 0 · 𝑥 ) )
59 oveq2 ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = ( 1 − 0 ) )
60 1m0e1 ⊢ ( 1 − 0 ) = 1
61 59 60 eqtrdi ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = 1 )
62 61 oveq1d ⊢ ( 𝑡 = 0 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( 1 · 𝑦 ) )
63 58 62 oveq12d ⊢ ( 𝑡 = 0 → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) )
64 eqid ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
65 ovex ⊢ ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) ∈ V
66 63 64 65 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) )
67 57 66 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) )
68 19 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑥 ∈ ℂ )
69 68 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 · 𝑥 ) = 0 )
70 38 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑦 ) = 𝑦 )
71 69 70 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = ( 0 + 𝑦 ) )
72 38 addlidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 + 𝑦 ) = 𝑦 )
73 71 72 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = 𝑦 )
74 67 73 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 )
75 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
76 oveq1 ⊢ ( 𝑡 = 1 → ( 𝑡 · 𝑥 ) = ( 1 · 𝑥 ) )
77 oveq2 ⊢ ( 𝑡 = 1 → ( 1 − 𝑡 ) = ( 1 − 1 ) )
78 1m1e0 ⊢ ( 1 − 1 ) = 0
79 77 78 eqtrdi ⊢ ( 𝑡 = 1 → ( 1 − 𝑡 ) = 0 )
80 79 oveq1d ⊢ ( 𝑡 = 1 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( 0 · 𝑦 ) )
81 76 80 oveq12d ⊢ ( 𝑡 = 1 → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) )
82 ovex ⊢ ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) ∈ V
83 81 64 82 fvmpt ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) )
84 75 83 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) )
85 68 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑥 ) = 𝑥 )
86 38 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 · 𝑦 ) = 0 )
87 85 86 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = ( 𝑥 + 0 ) )
88 68 addridd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑥 + 0 ) = 𝑥 )
89 87 88 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = 𝑥 )
90 84 89 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 )
91 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) )
92 91 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( 𝑓 ‘ 0 ) = 𝑦 ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ) )
93 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( 𝑓 ‘ 1 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) )
94 93 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( 𝑓 ‘ 1 ) = 𝑥 ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) )
95 92 94 anbi12d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) ) )
96 95 rspcev ⊢ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
97 56 74 90 96 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
98 97 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
99 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
100 13 1 99 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
101 4 100 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑆 ) )
102 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝐾 )
103 101 102 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝐾 )
104 103 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
105 103 104 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
106 98 105 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
107 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
108 107 ispconn ⊢ ( 𝐾 ∈ PConn ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
109 11 106 108 sylanbrc ⊢ ( 𝜑 → 𝐾 ∈ PConn )