sepfsepc

Description: If two sets are separated by a continuous function, then they are separated by closed neighborhoods. (Contributed by Zhi Wang, 9-Sep-2024)

		Ref	Expression
	Hypothesis	sepfsepc.1	$⊢ φ \to \exists f \in (J Cn II) (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])$
	Assertion	sepfsepc	$⊢ φ \to \exists n \in nei (J) (S) \exists m \in nei (J) (T) (n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		sepfsepc.1	$⊢ φ \to \exists f \in (J Cn II) (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])$
2		simpl	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f \in (J Cn II)$
3		0re	$⊢ 0 \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5		0le0	$⊢ 0 \leq 0$
6		3re	$⊢ 3 \in ℝ$
7		3ne0	$⊢ 3 \neq 0$
8	6 7	rereccli	$⊢ \frac{1}{3} \in ℝ$
9		1lt3	$⊢ 1 < 3$
10		recgt1i	$⊢ (3 \in ℝ \land 1 < 3) \to (0 < \frac{1}{3} \land \frac{1}{3} < 1)$
11	6 9 10	mp2an	$⊢ (0 < \frac{1}{3} \land \frac{1}{3} < 1)$
12	11	simpri	$⊢ \frac{1}{3} < 1$
13	8 4 12	ltleii	$⊢ \frac{1}{3} \leq 1$
14		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq 0 \land \frac{1}{3} \leq 1)) \to [0, \frac{1}{3}] \subseteq [0, 1]$
15	3 4 5 13 14	mp4an	$⊢ [0, \frac{1}{3}] \subseteq [0, 1]$
16		i0oii	$⊢ \frac{1}{3} \leq 1 \to [0, \frac{1}{3}) \in II$
17	13 16	ax-mp	$⊢ [0, \frac{1}{3}) \in II$
18	11	simpli	$⊢ 0 < \frac{1}{3}$
19	8	rexri	$⊢ \frac{1}{3} \in ℝ^{*}$
20		elico2	$⊢ (0 \in ℝ \land \frac{1}{3} \in ℝ^{*}) \to (0 \in [0, \frac{1}{3}) \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 < \frac{1}{3}))$
21	3 19 20	mp2an	$⊢ 0 \in [0, \frac{1}{3}) \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 < \frac{1}{3})$
22	21	biimpri	$⊢ (0 \in ℝ \land 0 \leq 0 \land 0 < \frac{1}{3}) \to 0 \in [0, \frac{1}{3})$
23	22	snssd	$⊢ (0 \in ℝ \land 0 \leq 0 \land 0 < \frac{1}{3}) \to \{0\} \subseteq [0, \frac{1}{3})$
24	3 5 18 23	mp3an	$⊢ \{0\} \subseteq [0, \frac{1}{3})$
25		icossicc	$⊢ [0, \frac{1}{3}) \subseteq [0, \frac{1}{3}]$
26	24 25	pm3.2i	$⊢ (\{0\} \subseteq [0, \frac{1}{3}) \land [0, \frac{1}{3}) \subseteq [0, \frac{1}{3}])$
27		sseq2	$⊢ g = [0, \frac{1}{3}) \to (\{0\} \subseteq g \leftrightarrow \{0\} \subseteq [0, \frac{1}{3}))$
28		sseq1	$⊢ g = [0, \frac{1}{3}) \to (g \subseteq [0, \frac{1}{3}] \leftrightarrow [0, \frac{1}{3}) \subseteq [0, \frac{1}{3}])$
29	27 28	anbi12d	$⊢ g = [0, \frac{1}{3}) \to ((\{0\} \subseteq g \land g \subseteq [0, \frac{1}{3}]) \leftrightarrow (\{0\} \subseteq [0, \frac{1}{3}) \land [0, \frac{1}{3}) \subseteq [0, \frac{1}{3}]))$
30	29	rspcev	$⊢ ([0, \frac{1}{3}) \in II \land (\{0\} \subseteq [0, \frac{1}{3}) \land [0, \frac{1}{3}) \subseteq [0, \frac{1}{3}])) \to \exists g \in II (\{0\} \subseteq g \land g \subseteq [0, \frac{1}{3}])$
31	17 26 30	mp2an	$⊢ \exists g \in II (\{0\} \subseteq g \land g \subseteq [0, \frac{1}{3}])$
32		iitop	$⊢ II \in Top$
33	24 25	sstri	$⊢ \{0\} \subseteq [0, \frac{1}{3}]$
34	33 15	sstri	$⊢ \{0\} \subseteq [0, 1]$
35		iiuni	$⊢ [0, 1] = ⋃ II$
36	35	isnei	$⊢ (II \in Top \land \{0\} \subseteq [0, 1]) \to ([0, \frac{1}{3}] \in nei (II) (\{0\}) \leftrightarrow ([0, \frac{1}{3}] \subseteq [0, 1] \land \exists g \in II (\{0\} \subseteq g \land g \subseteq [0, \frac{1}{3}])))$
37	32 34 36	mp2an	$⊢ [0, \frac{1}{3}] \in nei (II) (\{0\}) \leftrightarrow ([0, \frac{1}{3}] \subseteq [0, 1] \land \exists g \in II (\{0\} \subseteq g \land g \subseteq [0, \frac{1}{3}]))$
38	15 31 37	mpbir2an	$⊢ [0, \frac{1}{3}] \in nei (II) (\{0\})$
39	38	a1i	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to [0, \frac{1}{3}] \in nei (II) (\{0\})$
40		simprl	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to S \subseteq f^{-1} [\{0\}]$
41	2 39 40	cnneiima	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[0, \frac{1}{3}]] \in nei (J) (S)$
42		halfge0	$⊢ 0 \leq \frac{1}{2}$
43		1le1	$⊢ 1 \leq 1$
44		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq \frac{1}{2} \land 1 \leq 1)) \to [\frac{1}{2}, 1] \subseteq [0, 1]$
45	3 4 42 43 44	mp4an	$⊢ [\frac{1}{2}, 1] \subseteq [0, 1]$
46		io1ii	$⊢ 0 \leq \frac{1}{2} \to (\frac{1}{2}, 1] \in II$
47	42 46	ax-mp	$⊢ (\frac{1}{2}, 1] \in II$
48		halflt1	$⊢ \frac{1}{2} < 1$
49		halfre	$⊢ \frac{1}{2} \in ℝ$
50	49	rexri	$⊢ \frac{1}{2} \in ℝ^{*}$
51		elioc2	$⊢ (\frac{1}{2} \in ℝ^{*} \land 1 \in ℝ) \to (1 \in (\frac{1}{2}, 1] \leftrightarrow (1 \in ℝ \land \frac{1}{2} < 1 \land 1 \leq 1))$
52	50 4 51	mp2an	$⊢ 1 \in (\frac{1}{2}, 1] \leftrightarrow (1 \in ℝ \land \frac{1}{2} < 1 \land 1 \leq 1)$
53	52	biimpri	$⊢ (1 \in ℝ \land \frac{1}{2} < 1 \land 1 \leq 1) \to 1 \in (\frac{1}{2}, 1]$
54	53	snssd	$⊢ (1 \in ℝ \land \frac{1}{2} < 1 \land 1 \leq 1) \to \{1\} \subseteq (\frac{1}{2}, 1]$
55	4 48 43 54	mp3an	$⊢ \{1\} \subseteq (\frac{1}{2}, 1]$
56		iocssicc	$⊢ (\frac{1}{2}, 1] \subseteq [\frac{1}{2}, 1]$
57	55 56	pm3.2i	$⊢ (\{1\} \subseteq (\frac{1}{2}, 1] \land (\frac{1}{2}, 1] \subseteq [\frac{1}{2}, 1])$
58		sseq2	$⊢ h = (\frac{1}{2}, 1] \to (\{1\} \subseteq h \leftrightarrow \{1\} \subseteq (\frac{1}{2}, 1])$
59		sseq1	$⊢ h = (\frac{1}{2}, 1] \to (h \subseteq [\frac{1}{2}, 1] \leftrightarrow (\frac{1}{2}, 1] \subseteq [\frac{1}{2}, 1])$
60	58 59	anbi12d	$⊢ h = (\frac{1}{2}, 1] \to ((\{1\} \subseteq h \land h \subseteq [\frac{1}{2}, 1]) \leftrightarrow (\{1\} \subseteq (\frac{1}{2}, 1] \land (\frac{1}{2}, 1] \subseteq [\frac{1}{2}, 1]))$
61	60	rspcev	$⊢ ((\frac{1}{2}, 1] \in II \land (\{1\} \subseteq (\frac{1}{2}, 1] \land (\frac{1}{2}, 1] \subseteq [\frac{1}{2}, 1])) \to \exists h \in II (\{1\} \subseteq h \land h \subseteq [\frac{1}{2}, 1])$
62	47 57 61	mp2an	$⊢ \exists h \in II (\{1\} \subseteq h \land h \subseteq [\frac{1}{2}, 1])$
63	55 56	sstri	$⊢ \{1\} \subseteq [\frac{1}{2}, 1]$
64	63 45	sstri	$⊢ \{1\} \subseteq [0, 1]$
65	35	isnei	$⊢ (II \in Top \land \{1\} \subseteq [0, 1]) \to ([\frac{1}{2}, 1] \in nei (II) (\{1\}) \leftrightarrow ([\frac{1}{2}, 1] \subseteq [0, 1] \land \exists h \in II (\{1\} \subseteq h \land h \subseteq [\frac{1}{2}, 1])))$
66	32 64 65	mp2an	$⊢ [\frac{1}{2}, 1] \in nei (II) (\{1\}) \leftrightarrow ([\frac{1}{2}, 1] \subseteq [0, 1] \land \exists h \in II (\{1\} \subseteq h \land h \subseteq [\frac{1}{2}, 1]))$
67	45 62 66	mpbir2an	$⊢ [\frac{1}{2}, 1] \in nei (II) (\{1\})$
68	67	a1i	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to [\frac{1}{2}, 1] \in nei (II) (\{1\})$
69		simprr	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to T \subseteq f^{-1} [\{1\}]$
70	2 68 69	cnneiima	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[\frac{1}{2}, 1]] \in nei (J) (T)$
71		icccldii	$⊢ (0 \leq 0 \land \frac{1}{3} \leq 1) \to [0, \frac{1}{3}] \in Clsd (II)$
72	5 13 71	mp2an	$⊢ [0, \frac{1}{3}] \in Clsd (II)$
73		cnclima	$⊢ (f \in (J Cn II) \land [0, \frac{1}{3}] \in Clsd (II)) \to f^{-1} [[0, \frac{1}{3}]] \in Clsd (J)$
74	2 72 73	sylancl	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[0, \frac{1}{3}]] \in Clsd (J)$
75		icccldii	$⊢ (0 \leq \frac{1}{2} \land 1 \leq 1) \to [\frac{1}{2}, 1] \in Clsd (II)$
76	42 43 75	mp2an	$⊢ [\frac{1}{2}, 1] \in Clsd (II)$
77		cnclima	$⊢ (f \in (J Cn II) \land [\frac{1}{2}, 1] \in Clsd (II)) \to f^{-1} [[\frac{1}{2}, 1]] \in Clsd (J)$
78	2 76 77	sylancl	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[\frac{1}{2}, 1]] \in Clsd (J)$
79		eqid	$⊢ ⋃ J = ⋃ J$
80	79 35	cnf	$⊢ f \in (J Cn II) \to f : ⋃ J ⟶ [0, 1]$
81	80	ffund	$⊢ f \in (J Cn II) \to Fun f$
82	2 81	syl	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to Fun f$
83		0xr	$⊢ 0 \in ℝ^{*}$
84		1xr	$⊢ 1 \in ℝ^{*}$
85		2lt3	$⊢ 2 < 3$
86		2re	$⊢ 2 \in ℝ$
87		2pos	$⊢ 0 < 2$
88		3pos	$⊢ 0 < 3$
89	86 6 87 88	ltrecii	$⊢ 2 < 3 \leftrightarrow \frac{1}{3} < \frac{1}{2}$
90	85 89	mpbi	$⊢ \frac{1}{3} < \frac{1}{2}$
91		iccdisj2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land \frac{1}{3} < \frac{1}{2}) \to [0, \frac{1}{3}] \cap [\frac{1}{2}, 1] = \emptyset$
92	83 84 90 91	mp3an	$⊢ [0, \frac{1}{3}] \cap [\frac{1}{2}, 1] = \emptyset$
93	92	a1i	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to [0, \frac{1}{3}] \cap [\frac{1}{2}, 1] = \emptyset$
94		ssidd	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[0, \frac{1}{3}]] \subseteq f^{-1} [[0, \frac{1}{3}]]$
95		ssidd	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[\frac{1}{2}, 1]] \subseteq f^{-1} [[\frac{1}{2}, 1]]$
96	82 93 94 95	predisj	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to f^{-1} [[0, \frac{1}{3}]] \cap f^{-1} [[\frac{1}{2}, 1]] = \emptyset$
97		eleq1	$⊢ n = f^{-1} [[0, \frac{1}{3}]] \to (n \in Clsd (J) \leftrightarrow f^{-1} [[0, \frac{1}{3}]] \in Clsd (J))$
98		ineq1	$⊢ n = f^{-1} [[0, \frac{1}{3}]] \to n \cap m = f^{-1} [[0, \frac{1}{3}]] \cap m$
99	98	eqeq1d	$⊢ n = f^{-1} [[0, \frac{1}{3}]] \to (n \cap m = \emptyset \leftrightarrow f^{-1} [[0, \frac{1}{3}]] \cap m = \emptyset)$
100	97 99	3anbi13d	$⊢ n = f^{-1} [[0, \frac{1}{3}]] \to ((n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset) \leftrightarrow (f^{-1} [[0, \frac{1}{3}]] \in Clsd (J) \land m \in Clsd (J) \land f^{-1} [[0, \frac{1}{3}]] \cap m = \emptyset))$
101		eleq1	$⊢ m = f^{-1} [[\frac{1}{2}, 1]] \to (m \in Clsd (J) \leftrightarrow f^{-1} [[\frac{1}{2}, 1]] \in Clsd (J))$
102		ineq2	$⊢ m = f^{-1} [[\frac{1}{2}, 1]] \to f^{-1} [[0, \frac{1}{3}]] \cap m = f^{-1} [[0, \frac{1}{3}]] \cap f^{-1} [[\frac{1}{2}, 1]]$
103	102	eqeq1d	$⊢ m = f^{-1} [[\frac{1}{2}, 1]] \to (f^{-1} [[0, \frac{1}{3}]] \cap m = \emptyset \leftrightarrow f^{-1} [[0, \frac{1}{3}]] \cap f^{-1} [[\frac{1}{2}, 1]] = \emptyset)$
104	101 103	3anbi23d	$⊢ m = f^{-1} [[\frac{1}{2}, 1]] \to ((f^{-1} [[0, \frac{1}{3}]] \in Clsd (J) \land m \in Clsd (J) \land f^{-1} [[0, \frac{1}{3}]] \cap m = \emptyset) \leftrightarrow (f^{-1} [[0, \frac{1}{3}]] \in Clsd (J) \land f^{-1} [[\frac{1}{2}, 1]] \in Clsd (J) \land f^{-1} [[0, \frac{1}{3}]] \cap f^{-1} [[\frac{1}{2}, 1]] = \emptyset))$
105	100 104	rspc2ev	$⊢ (f^{-1} [[0, \frac{1}{3}]] \in nei (J) (S) \land f^{-1} [[\frac{1}{2}, 1]] \in nei (J) (T) \land (f^{-1} [[0, \frac{1}{3}]] \in Clsd (J) \land f^{-1} [[\frac{1}{2}, 1]] \in Clsd (J) \land f^{-1} [[0, \frac{1}{3}]] \cap f^{-1} [[\frac{1}{2}, 1]] = \emptyset)) \to \exists n \in nei (J) (S) \exists m \in nei (J) (T) (n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset)$
106	41 70 74 78 96 105	syl113anc	$⊢ (f \in (J Cn II) \land (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}])) \to \exists n \in nei (J) (S) \exists m \in nei (J) (T) (n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset)$
107	106	rexlimiva	$⊢ \exists f \in (J Cn II) (S \subseteq f^{-1} [\{0\}] \land T \subseteq f^{-1} [\{1\}]) \to \exists n \in nei (J) (S) \exists m \in nei (J) (T) (n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset)$
108	1 107	syl	$⊢ φ \to \exists n \in nei (J) (S) \exists m \in nei (J) (T) (n \in Clsd (J) \land m \in Clsd (J) \land n \cap m = \emptyset)$

Metamath Proof Explorer

Theorem sepfsepc

Proof