reconnlem1

Description: Lemma for reconn . Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Assertion	reconnlem1	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to [X, Y] \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to topGen (ran (.)) ↾_{𝑡} A \in Conn$
2		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
3	2	a1i	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to topGen (ran (.)) \in TopOn (ℝ)$
4		simplll	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to A \subseteq ℝ$
5		iooretop	$⊢ (−∞, z) \in topGen (ran (.))$
6	5	a1i	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (−∞, z) \in topGen (ran (.))$
7		iooretop	$⊢ (z, +∞) \in topGen (ran (.))$
8	7	a1i	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z, +∞) \in topGen (ran (.))$
9		simplrl	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to X \in A$
10	4 9	sseldd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to X \in ℝ$
11	10	mnfltd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to −∞ < X$
12		eldifn	$⊢ z \in ([X, Y] ∖ A) \to \neg z \in A$
13	12	adantl	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to \neg z \in A$
14		eleq1	$⊢ X = z \to (X \in A \leftrightarrow z \in A)$
15	9 14	syl5ibcom	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (X = z \to z \in A)$
16	13 15	mtod	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to \neg X = z$
17		eldifi	$⊢ z \in ([X, Y] ∖ A) \to z \in [X, Y]$
18	17	adantl	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z \in [X, Y]$
19		simplrr	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to Y \in A$
20	4 19	sseldd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to Y \in ℝ$
21		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (z \in [X, Y] \leftrightarrow (z \in ℝ \land X \leq z \land z \leq Y))$
22	10 20 21	syl2anc	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z \in [X, Y] \leftrightarrow (z \in ℝ \land X \leq z \land z \leq Y))$
23	18 22	mpbid	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z \in ℝ \land X \leq z \land z \leq Y)$
24	23	simp2d	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to X \leq z$
25	23	simp1d	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z \in ℝ$
26	10 25	leloed	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (X \leq z \leftrightarrow (X < z \lor X = z))$
27	24 26	mpbid	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (X < z \lor X = z)$
28	27	ord	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (\neg X < z \to X = z)$
29	16 28	mt3d	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to X < z$
30		mnfxr	$⊢ −∞ \in ℝ^{*}$
31	25	rexrd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z \in ℝ^{*}$
32		elioo2	$⊢ (−∞ \in ℝ^{} \land z \in ℝ^{}) \to (X \in (−∞, z) \leftrightarrow (X \in ℝ \land −∞ < X \land X < z))$
33	30 31 32	sylancr	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (X \in (−∞, z) \leftrightarrow (X \in ℝ \land −∞ < X \land X < z))$
34	10 11 29 33	mpbir3and	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to X \in (−∞, z)$
35		inelcm	$⊢ (X \in (−∞, z) \land X \in A) \to (−∞, z) \cap A \neq \emptyset$
36	34 9 35	syl2anc	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (−∞, z) \cap A \neq \emptyset$
37		eleq1	$⊢ z = Y \to (z \in A \leftrightarrow Y \in A)$
38	19 37	syl5ibrcom	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z = Y \to z \in A)$
39	13 38	mtod	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to \neg z = Y$
40	23	simp3d	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z \leq Y$
41	25 20	leloed	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z \leq Y \leftrightarrow (z < Y \lor z = Y))$
42	40 41	mpbid	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z < Y \lor z = Y)$
43	42	ord	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (\neg z < Y \to z = Y)$
44	39 43	mt3d	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z < Y$
45	20	ltpnfd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to Y < +∞$
46		pnfxr	$⊢ +∞ \in ℝ^{*}$
47		elioo2	$⊢ (z \in ℝ^{} \land +∞ \in ℝ^{}) \to (Y \in (z, +∞) \leftrightarrow (Y \in ℝ \land z < Y \land Y < +∞))$
48	31 46 47	sylancl	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (Y \in (z, +∞) \leftrightarrow (Y \in ℝ \land z < Y \land Y < +∞))$
49	20 44 45 48	mpbir3and	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to Y \in (z, +∞)$
50		inelcm	$⊢ (Y \in (z, +∞) \land Y \in A) \to (z, +∞) \cap A \neq \emptyset$
51	49 19 50	syl2anc	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z, +∞) \cap A \neq \emptyset$
52		inss1	$⊢ ((−∞, z) \cap (z, +∞)) \cap A \subseteq (−∞, z) \cap (z, +∞)$
53	31 30	jctil	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (−∞ \in ℝ^{} \land z \in ℝ^{})$
54	31 46	jctir	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (z \in ℝ^{} \land +∞ \in ℝ^{})$
55	25	leidd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z \leq z$
56		ioodisj	$⊢ (((−∞ \in ℝ^{} \land z \in ℝ^{}) \land (z \in ℝ^{} \land +∞ \in ℝ^{})) \land z \leq z) \to (−∞, z) \cap (z, +∞) = \emptyset$
57	53 54 55 56	syl21anc	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (−∞, z) \cap (z, +∞) = \emptyset$
58		sseq0	$⊢ (((−∞, z) \cap (z, +∞)) \cap A \subseteq (−∞, z) \cap (z, +∞) \land (−∞, z) \cap (z, +∞) = \emptyset) \to ((−∞, z) \cap (z, +∞)) \cap A = \emptyset$
59	52 57 58	sylancr	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to ((−∞, z) \cap (z, +∞)) \cap A = \emptyset$
60	30	a1i	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to −∞ \in ℝ^{*}$
61	46	a1i	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to +∞ \in ℝ^{*}$
62	25	mnfltd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to −∞ < z$
63	25	ltpnfd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to z < +∞$
64		ioojoin	$⊢ ((−∞ \in ℝ^{} \land z \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ < z \land z < +∞)) \to ((−∞, z) \cup \{z\}) \cup (z, +∞) = (−∞, +∞)$
65	60 31 61 62 63 64	syl32anc	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to ((−∞, z) \cup \{z\}) \cup (z, +∞) = (−∞, +∞)$
66		unass	$⊢ ((−∞, z) \cup \{z\}) \cup (z, +∞) = (−∞, z) \cup (\{z\} \cup (z, +∞))$
67		un12	$⊢ (−∞, z) \cup (\{z\} \cup (z, +∞)) = \{z\} \cup ((−∞, z) \cup (z, +∞))$
68	66 67	eqtri	$⊢ ((−∞, z) \cup \{z\}) \cup (z, +∞) = \{z\} \cup ((−∞, z) \cup (z, +∞))$
69		ioomax	$⊢ (−∞, +∞) = ℝ$
70	65 68 69	3eqtr3g	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to \{z\} \cup ((−∞, z) \cup (z, +∞)) = ℝ$
71	4 70	sseqtrrd	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to A \subseteq \{z\} \cup ((−∞, z) \cup (z, +∞))$
72		disjsn	$⊢ A \cap \{z\} = \emptyset \leftrightarrow \neg z \in A$
73	13 72	sylibr	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to A \cap \{z\} = \emptyset$
74		disjssun	$⊢ A \cap \{z\} = \emptyset \to (A \subseteq \{z\} \cup ((−∞, z) \cup (z, +∞)) \leftrightarrow A \subseteq (−∞, z) \cup (z, +∞))$
75	73 74	syl	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to (A \subseteq \{z\} \cup ((−∞, z) \cup (z, +∞)) \leftrightarrow A \subseteq (−∞, z) \cup (z, +∞))$
76	71 75	mpbid	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to A \subseteq (−∞, z) \cup (z, +∞)$
77	3 4 6 8 36 51 59 76	nconnsubb	$⊢ (((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \land z \in ([X, Y] ∖ A)) \to \neg topGen (ran (.)) ↾_{𝑡} A \in Conn$
78	77	ex	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to (z \in ([X, Y] ∖ A) \to \neg topGen (ran (.)) ↾_{𝑡} A \in Conn)$
79	1 78	mt2d	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to \neg z \in ([X, Y] ∖ A)$
80	79	eq0rdv	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to [X, Y] ∖ A = \emptyset$
81		ssdif0	$⊢ [X, Y] \subseteq A \leftrightarrow [X, Y] ∖ A = \emptyset$
82	80 81	sylibr	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (X \in A \land Y \in A)) \to [X, Y] \subseteq A$

Metamath Proof Explorer

Theorem reconnlem1

Proof