Metamath Proof Explorer

Theorem cvxpconn

Description: A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015)

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 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
16 ax-resscn ⊢ ℝ ⊆ ℂ
17 15 16 sstri ⊢ ( 0 [,] 1 ) ⊆ ℂ
18 17 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 [,] 1 ) ⊆ ℂ )
19 14 cnmptid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( 𝐽 Cn 𝐽 ) )
20 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑆 ⊆ ℂ )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
22 20 21 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑥 ∈ ℂ )
23 14 14 22 cnmptc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
24 3 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
25 24 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
26 14 19 23 25 cnmpt12f ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
27 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 1 ∈ ℂ )
28 14 14 27 cnmptc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ 1 ) ∈ ( 𝐽 Cn 𝐽 ) )
29 3 subcn ⊢ − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
30 29 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
31 14 28 19 30 cnmpt12f ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( 1 − 𝑡 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
32 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
33 20 32 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → 𝑦 ∈ ℂ )
34 14 14 33 cnmptc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
35 14 31 34 25 cnmpt12f ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
36 3 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
37 36 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
38 14 26 35 37 cnmpt12f ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ℂ ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
39 12 14 18 38 cnmpt1res ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) )
40 2 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → ( 𝑦 ∈ 𝑆 → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) ) ) )
41 40 com23 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) ) ) )
42 41 imp42 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
43 42 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) : ( 0 [,] 1 ) ⟶ 𝑆 )
44 43 frnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ran ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ⊆ 𝑆 )
45 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ⊆ 𝑆 ∧ 𝑆 ⊆ ℂ ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) ) )
46 14 44 20 45 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐽 ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) ) )
47 39 46 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) )
48 4 oveq2i ⊢ ( II Cn 𝐾 ) = ( II Cn ( 𝐽 ↾t 𝑆 ) )
49 47 48 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐾 ) )
50 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
51 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 · 𝑥 ) = ( 0 · 𝑥 ) )
52 oveq2 ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = ( 1 − 0 ) )
53 1m0e1 ⊢ ( 1 − 0 ) = 1
54 52 53 eqtrdi ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = 1 )
55 54 oveq1d ⊢ ( 𝑡 = 0 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( 1 · 𝑦 ) )
56 51 55 oveq12d ⊢ ( 𝑡 = 0 → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) )
57 eqid ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
58 ovex ⊢ ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) ∈ V
59 56 57 58 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) )
60 50 59 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) )
61 22 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 · 𝑥 ) = 0 )
62 33 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑦 ) = 𝑦 )
63 61 62 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = ( 0 + 𝑦 ) )
64 33 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 + 𝑦 ) = 𝑦 )
65 63 64 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = 𝑦 )
66 60 65 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 )
67 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
68 oveq1 ⊢ ( 𝑡 = 1 → ( 𝑡 · 𝑥 ) = ( 1 · 𝑥 ) )
69 oveq2 ⊢ ( 𝑡 = 1 → ( 1 − 𝑡 ) = ( 1 − 1 ) )
70 1m1e0 ⊢ ( 1 − 1 ) = 0
71 69 70 eqtrdi ⊢ ( 𝑡 = 1 → ( 1 − 𝑡 ) = 0 )
72 71 oveq1d ⊢ ( 𝑡 = 1 → ( ( 1 − 𝑡 ) · 𝑦 ) = ( 0 · 𝑦 ) )
73 68 72 oveq12d ⊢ ( 𝑡 = 1 → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) )
74 ovex ⊢ ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) ∈ V
75 73 57 74 fvmpt ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) )
76 67 75 ax-mp ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) )
77 22 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑥 ) = 𝑥 )
78 33 mul02d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 · 𝑦 ) = 0 )
79 77 78 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = ( 𝑥 + 0 ) )
80 22 addid1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑥 + 0 ) = 𝑥 )
81 79 80 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = 𝑥 )
82 76 81 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 )
83 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) )
84 83 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( 𝑓 ‘ 0 ) = 𝑦 ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ) )
85 fveq1 ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( 𝑓 ‘ 1 ) = ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) )
86 85 eqeq1d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( 𝑓 ‘ 1 ) = 𝑥 ↔ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) )
87 84 86 anbi12d ⊢ ( 𝑓 = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) ) )
88 87 rspcev ⊢ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 0 ) = 𝑦 ∧ ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ‘ 1 ) = 𝑥 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
89 49 66 82 88 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
90 89 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
91 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
92 13 1 91 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
93 4 92 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑆 ) )
94 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝐾 )
95 93 94 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝐾 )
96 95 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
97 95 96 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ∀ 𝑥 ∈ 𝑆 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
98 90 97 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) )
99 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
100 99 ispconn ⊢ ( 𝐾 ∈ PConn ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑦 ∈ ∪ 𝐾 ∀ 𝑥 ∈ ∪ 𝐾 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) )
101 11 98 100 sylanbrc ⊢ ( 𝜑 → 𝐾 ∈ PConn )