iccllysconn

Description: A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	iccllysconn	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in LocallySConn$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to x \in topGen (ran (.))$
2		inss1	$⊢ x \cap [A, B] \subseteq x$
3		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to y \in (x \cap [A, B])$
4	2 3	sselid	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to y \in x$
5		tg2	$⊢ (x \in topGen (ran (.)) \land y \in x) \to \exists z \in ran (.) (y \in z \land z \subseteq x)$
6	1 4 5	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to \exists z \in ran (.) (y \in z \land z \subseteq x)$
7		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
8		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
9		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b))$
10	7 8 9	mp2b	$⊢ z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b)$
11		inss1	$⊢ z \cap [A, B] \subseteq z$
12		simprrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to z \subseteq x$
13	11 12	sstrid	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to z \cap [A, B] \subseteq x$
14		simprrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to y \in z$
15		simprl	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to z = (a, b)$
16	15	ineq1d	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to z \cap [A, B] = (a, b) \cap [A, B]$
17	16	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) = topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B])$
18		ioosconn	$⊢ topGen (ran (.)) ↾_{𝑡} (a, b) \in SConn$
19		ioossre	$⊢ (a, b) \subseteq ℝ$
20		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} (a, b) = topGen (ran (.)) ↾_{𝑡} (a, b)$
21	20	resconn	$⊢ (a, b) \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} (a, b) \in SConn \leftrightarrow topGen (ran (.)) ↾_{𝑡} (a, b) \in Conn)$
22		reconn	$⊢ (a, b) \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} (a, b) \in Conn \leftrightarrow \forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b))$
23	21 22	bitrd	$⊢ (a, b) \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} (a, b) \in SConn \leftrightarrow \forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b))$
24	19 23	ax-mp	$⊢ topGen (ran (.)) ↾_{𝑡} (a, b) \in SConn \leftrightarrow \forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b)$
25	18 24	mpbi	$⊢ \forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b)$
26		inss1	$⊢ (a, b) \cap [A, B] \subseteq (a, b)$
27		ssralv	$⊢ (a, b) \cap [A, B] \subseteq (a, b) \to (\forall v \in (a, b) [u, v] \subseteq (a, b) \to \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b))$
28	27	ralimdv	$⊢ (a, b) \cap [A, B] \subseteq (a, b) \to (\forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b) \to \forall u \in (a, b) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b))$
29		ssralv	$⊢ (a, b) \cap [A, B] \subseteq (a, b) \to (\forall u \in (a, b) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b))$
30	28 29	syld	$⊢ (a, b) \cap [A, B] \subseteq (a, b) \to (\forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b))$
31	26 30	ax-mp	$⊢ \forall u \in (a, b) \forall v \in (a, b) [u, v] \subseteq (a, b) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b)$
32	25 31	mp1i	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b)$
33		inss2	$⊢ (a, b) \cap [A, B] \subseteq [A, B]$
34		iccconn	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn$
35		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
36		reconn	$⊢ [A, B] \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn \leftrightarrow \forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B])$
37	35 36	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn \leftrightarrow \forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B])$
38	34 37	mpbid	$⊢ (A \in ℝ \land B \in ℝ) \to \forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B]$
39	38	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to \forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B]$
40		ssralv	$⊢ (a, b) \cap [A, B] \subseteq [A, B] \to (\forall v \in [A, B] [u, v] \subseteq [A, B] \to \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
41	40	ralimdv	$⊢ (a, b) \cap [A, B] \subseteq [A, B] \to (\forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B] \to \forall u \in [A, B] \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
42		ssralv	$⊢ (a, b) \cap [A, B] \subseteq [A, B] \to (\forall u \in [A, B] \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B] \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
43	41 42	syld	$⊢ (a, b) \cap [A, B] \subseteq [A, B] \to (\forall u \in [A, B] \forall v \in [A, B] [u, v] \subseteq [A, B] \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
44	33 39 43	mpsyl	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B]$
45		ssin	$⊢ ([u, v] \subseteq (a, b) \land [u, v] \subseteq [A, B]) \leftrightarrow [u, v] \subseteq (a, b) \cap [A, B]$
46	45	2ralbii	$⊢ \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) ([u, v] \subseteq (a, b) \land [u, v] \subseteq [A, B]) \leftrightarrow \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B]$
47		r19.26-2	$⊢ \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) ([u, v] \subseteq (a, b) \land [u, v] \subseteq [A, B]) \leftrightarrow (\forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \land \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
48	46 47	bitr3i	$⊢ \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B] \leftrightarrow (\forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \land \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq [A, B])$
49	32 44 48	sylanbrc	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B]$
50	26 19	sstri	$⊢ (a, b) \cap [A, B] \subseteq ℝ$
51		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) = topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B])$
52	51	resconn	$⊢ (a, b) \cap [A, B] \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in SConn \leftrightarrow topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in Conn)$
53		reconn	$⊢ (a, b) \cap [A, B] \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in Conn \leftrightarrow \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B])$
54	52 53	bitrd	$⊢ (a, b) \cap [A, B] \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in SConn \leftrightarrow \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B])$
55	50 54	ax-mp	$⊢ topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in SConn \leftrightarrow \forall u \in ((a, b) \cap [A, B]) \forall v \in ((a, b) \cap [A, B]) [u, v] \subseteq (a, b) \cap [A, B]$
56	49 55	sylibr	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to topGen (ran (.)) ↾_{𝑡} ((a, b) \cap [A, B]) \in SConn$
57	17 56	eqeltrd	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn$
58	13 14 57	3jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \land (z = (a, b) \land (y \in z \land z \subseteq x))) \to (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)$
59	58	exp32	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (z = (a, b) \to ((y \in z \land z \subseteq x) \to (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)))$
60	59	rexlimdvw	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (\exists b \in ℝ^{*} z = (a, b) \to ((y \in z \land z \subseteq x) \to (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)))$
61	60	rexlimdvw	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (\exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b) \to ((y \in z \land z \subseteq x) \to (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)))$
62	10 61	syl5bi	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (z \in ran (.) \to ((y \in z \land z \subseteq x) \to (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)))$
63	62	reximdvai	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (\exists z \in ran (.) (y \in z \land z \subseteq x) \to \exists z \in ran (.) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn))$
64		retopbas	$⊢ ran (.) \in TopBases$
65		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
66		ssrexv	$⊢ ran (.) \subseteq topGen (ran (.)) \to (\exists z \in ran (.) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn) \to \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn))$
67	64 65 66	mp2b	$⊢ \exists z \in ran (.) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn) \to \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)$
68	63 67	syl6	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to (\exists z \in ran (.) (y \in z \land z \subseteq x) \to \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn))$
69	6 68	mpd	$⊢ ((A \in ℝ \land B \in ℝ) \land (x \in topGen (ran (.)) \land y \in (x \cap [A, B]))) \to \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)$
70	69	ralrimivva	$⊢ (A \in ℝ \land B \in ℝ) \to \forall x \in topGen (ran (.)) \forall y \in (x \cap [A, B]) \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)$
71		retop	$⊢ topGen (ran (.)) \in Top$
72		ovex	$⊢ [A, B] \in V$
73		subislly	$⊢ (topGen (ran (.)) \in Top \land [A, B] \in V) \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in LocallySConn\leftrightarrow\forall x \in topGen (ran (.)) \forall y \in (x \cap [A, B]) \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn))$
74	71 72 73	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] \in LocallySConn\leftrightarrow\forall x \in topGen (ran (.)) \forall y \in (x \cap [A, B]) \exists z \in topGen (ran (.)) (z \cap [A, B] \subseteq x \land y \in z \land topGen (ran (.)) ↾_{𝑡} (z \cap [A, B]) \in SConn)$
75	70 74	sylibr	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in LocallySConn$

Metamath Proof Explorer

Theorem iccllysconn

Proof