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	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑦 ) = 𝑦 )
63	61 62	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = ( 0 + 𝑦 ) )
64	33	addlidd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 + 𝑦 ) = 𝑦 )
65	63 64	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 0 · 𝑥 ) + ( 1 · 𝑦 ) ) = 𝑦 )
66	60 65	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 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	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 1 · 𝑥 ) = 𝑥 )
78	33	mul02d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 0 · 𝑦 ) = 0 )
79	77 78	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = ( 𝑥 + 0 ) )
80	22	addridd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑥 + 0 ) = 𝑥 )
81	79 80	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 1 · 𝑥 ) + ( 0 · 𝑦 ) ) = 𝑥 )
82	76 81	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝑡 ∈ ( 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 )

Metamath Proof Explorer

Theorem cvxpconn

Proof