reconn

Description: A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Assertion	reconn	$⊢ A \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \leftrightarrow \forall x \in A \forall y \in A [x, y] \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		reconnlem1	$⊢ ((A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \land (x \in A \land y \in A)) \to [x, y] \subseteq A$
2	1	ralrimivva	$⊢ (A \subseteq ℝ \land topGen (ran (.)) ↾_{𝑡} A \in Conn) \to \forall x \in A \forall y \in A [x, y] \subseteq A$
3	2	ex	$⊢ A \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \to \forall x \in A \forall y \in A [x, y] \subseteq A)$
4		n0	$⊢ u \cap A \neq \emptyset \leftrightarrow \exists b b \in (u \cap A)$
5		n0	$⊢ v \cap A \neq \emptyset \leftrightarrow \exists c c \in (v \cap A)$
6	4 5	anbi12i	$⊢ (u \cap A \neq \emptyset \land v \cap A \neq \emptyset) \leftrightarrow (\exists b b \in (u \cap A) \land \exists c c \in (v \cap A))$
7		exdistrv	$⊢ \exists b \exists c (b \in (u \cap A) \land c \in (v \cap A)) \leftrightarrow (\exists b b \in (u \cap A) \land \exists c c \in (v \cap A))$
8		simplll	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to A \subseteq ℝ$
9		simprll	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to b \in (u \cap A)$
10	9	elin2d	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to b \in A$
11	8 10	sseldd	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to b \in ℝ$
12		simprlr	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to c \in (v \cap A)$
13	12	elin2d	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to c \in A$
14	8 13	sseldd	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to c \in ℝ$
15	8	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to A \subseteq ℝ$
16		simplrl	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to u \in topGen (ran (.))$
17	16	ad2antrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to u \in topGen (ran (.))$
18		simplrr	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to v \in topGen (ran (.))$
19	18	ad2antrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to v \in topGen (ran (.))$
20		simpllr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to \forall x \in A \forall y \in A [x, y] \subseteq A$
21	9	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to b \in (u \cap A)$
22	12	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to c \in (v \cap A)$
23		simplrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to u \cap v \subseteq ℝ ∖ A$
24		simpr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to b \leq c$
25		eqid	$⊢ sup (u \cap [b, c] ℝ <) = sup (u \cap [b, c] ℝ <)$
26	15 17 19 20 21 22 23 24 25	reconnlem2	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land b \leq c) \to \neg A \subseteq u \cup v$
27	8	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to A \subseteq ℝ$
28	18	ad2antrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to v \in topGen (ran (.))$
29	16	ad2antrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to u \in topGen (ran (.))$
30		simpllr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to \forall x \in A \forall y \in A [x, y] \subseteq A$
31	12	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to c \in (v \cap A)$
32	9	adantr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to b \in (u \cap A)$
33		incom	$⊢ v \cap u = u \cap v$
34		simplrr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to u \cap v \subseteq ℝ ∖ A$
35	33 34	eqsstrid	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to v \cap u \subseteq ℝ ∖ A$
36		simpr	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to c \leq b$
37		eqid	$⊢ sup (v \cap [c, b] ℝ <) = sup (v \cap [c, b] ℝ <)$
38	27 28 29 30 31 32 35 36 37	reconnlem2	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to \neg A \subseteq v \cup u$
39		uncom	$⊢ v \cup u = u \cup v$
40	39	sseq2i	$⊢ A \subseteq v \cup u \leftrightarrow A \subseteq u \cup v$
41	38 40	sylnib	$⊢ ((((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \land c \leq b) \to \neg A \subseteq u \cup v$
42	11 14 26 41	lecasei	$⊢ (((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \land ((b \in (u \cap A) \land c \in (v \cap A)) \land u \cap v \subseteq ℝ ∖ A)) \to \neg A \subseteq u \cup v$
43	42	exp32	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to ((b \in (u \cap A) \land c \in (v \cap A)) \to (u \cap v \subseteq ℝ ∖ A \to \neg A \subseteq u \cup v))$
44	43	exlimdvv	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to (\exists b \exists c (b \in (u \cap A) \land c \in (v \cap A)) \to (u \cap v \subseteq ℝ ∖ A \to \neg A \subseteq u \cup v))$
45	7 44	syl5bir	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to ((\exists b b \in (u \cap A) \land \exists c c \in (v \cap A)) \to (u \cap v \subseteq ℝ ∖ A \to \neg A \subseteq u \cup v))$
46	6 45	syl5bi	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset) \to (u \cap v \subseteq ℝ ∖ A \to \neg A \subseteq u \cup v))$
47	46	expd	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to (u \cap A \neq \emptyset \to (v \cap A \neq \emptyset \to (u \cap v \subseteq ℝ ∖ A \to \neg A \subseteq u \cup v)))$
48	47	3impd	$⊢ ((A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset \land u \cap v \subseteq ℝ ∖ A) \to \neg A \subseteq u \cup v)$
49	48	ex	$⊢ (A \subseteq ℝ \land (u \in topGen (ran (.)) \land v \in topGen (ran (.)))) \to (\forall x \in A \forall y \in A [x, y] \subseteq A \to ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset \land u \cap v \subseteq ℝ ∖ A) \to \neg A \subseteq u \cup v))$
50	49	ralrimdvva	$⊢ A \subseteq ℝ \to (\forall x \in A \forall y \in A [x, y] \subseteq A \to \forall u \in topGen (ran (.)) \forall v \in topGen (ran (.)) ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset \land u \cap v \subseteq ℝ ∖ A) \to \neg A \subseteq u \cup v))$
51		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
52		connsub	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land A \subseteq ℝ) \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \leftrightarrow \forall u \in topGen (ran (.)) \forall v \in topGen (ran (.)) ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset \land u \cap v \subseteq ℝ ∖ A) \to \neg A \subseteq u \cup v))$
53	51 52	mpan	$⊢ A \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \leftrightarrow \forall u \in topGen (ran (.)) \forall v \in topGen (ran (.)) ((u \cap A \neq \emptyset \land v \cap A \neq \emptyset \land u \cap v \subseteq ℝ ∖ A) \to \neg A \subseteq u \cup v))$
54	50 53	sylibrd	$⊢ A \subseteq ℝ \to (\forall x \in A \forall y \in A [x, y] \subseteq A \to topGen (ran (.)) ↾_{𝑡} A \in Conn)$
55	3 54	impbid	$⊢ A \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \leftrightarrow \forall x \in A \forall y \in A [x, y] \subseteq A)$

Metamath Proof Explorer

Theorem reconn

Proof