Theorem iccllysconn 36136

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

Assertion

Ref	Expression
iccllysconn	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn)

Proof of Theorem iccllysconn

Dummy variables 𝑎 𝑏 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 783	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → 𝑥 ∈ (topGen‘ran (,)))
2		inss1 4135	. . . . . 6 ⊢ (𝑥 ∩ (𝐴[,]𝐵)) ⊆ 𝑥
3		simprr 785	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))
4	2, 3	sselid 3910	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ 𝑥)
5		tg2 23295	. . . . 5 ⊢ ((𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ ran (,)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))
6	1, 4, 5	syl2anc 596	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → ∃𝑧 ∈ ran (,)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))
7		ioof 13588	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		ffn 6717	. . . . . . . 8 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
9		ovelrn 7604	. . . . . . . 8 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏)))
10	7, 8, 9	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏))
11		inss1 4135	. . . . . . . . . . . 12 ⊢ (𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑧
12		simprrr 794	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → 𝑧 ⊆ 𝑥)
13	11, 12	sstrid 3923	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → (𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥)
14		simprrl 793	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → 𝑦 ∈ 𝑧)
15		simprl 783	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → 𝑧 = (𝑎(,)𝑏))
16	15	ineq1d 4118	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → (𝑧 ∩ (𝐴[,]𝐵)) = ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
17	16	oveq2d 7443	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))))
18		ioosconn 36133	. . . . . . . . . . . . . . . 16 ⊢ ((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ SConn
19		ioossre 13548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎(,)𝑏) ⊆ ℝ
20		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) = ((topGen‘ran (,)) ↾t (𝑎(,)𝑏))
21	20	resconn 36132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎(,)𝑏) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ SConn ↔ ((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ Conn))
22		reconn 25160	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎(,)𝑏) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ Conn ↔ ∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
23	21, 22	bitrd 282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ SConn ↔ ∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
24	19, 23	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (((topGen‘ran (,)) ↾t (𝑎(,)𝑏)) ∈ SConn ↔ ∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏))
25	18, 24	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ ∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)
26		inss1 4135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝑎(,)𝑏)
27		ssralv 3981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝑎(,)𝑏) → (∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) → ∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
28	27	ralimdv 3179	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝑎(,)𝑏) → (∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) → ∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
29		ssralv 3981	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝑎(,)𝑏) → (∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
30	28, 29	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝑎(,)𝑏) → (∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏)))
31	26, 30	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ (𝑎(,)𝑏)∀𝑣 ∈ (𝑎(,)𝑏)(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏))
32	25, 31	mp1i 14	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏))
33		inss2 4136	. . . . . . . . . . . . . . 15 ⊢ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵)
34		iccconn 25162	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
35		iccssre 13570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
36		reconn 25160	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn ↔ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
37	35, 36	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn ↔ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
38	34, 37	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵))
39	38	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵))
40		ssralv 3981	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵) → ∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
41	40	ralimdv 3179	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵) → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
42		ssralv 3981	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
43	41, 42	syld 48	. . . . . . . . . . . . . . 15 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑢 ∈ (𝐴[,]𝐵)∀𝑣 ∈ (𝐴[,]𝐵)(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
44	33, 39, 43	mpsyl 69	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵))
45		ssin 4137	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) ∧ (𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)) ↔ (𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
46	45	2ralbii 3140	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))((𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) ∧ (𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)) ↔ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
47		r19.26-2 3150	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))((𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) ∧ (𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)) ↔ (∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) ∧ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
48	46, 47	bitr3i 280	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ↔ (∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝑎(,)𝑏) ∧ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ (𝐴[,]𝐵)))
49	32, 44, 48	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
50	26, 19	sstri 3921	. . . . . . . . . . . . . 14 ⊢ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ ℝ
51		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
52	51	resconn 36132	. . . . . . . . . . . . . . 15 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ ℝ → (((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ SConn ↔ ((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ Conn))
53		reconn 25160	. . . . . . . . . . . . . . 15 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ ℝ → (((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ Conn ↔ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))))
54	52, 53	bitrd 282	. . . . . . . . . . . . . 14 ⊢ (((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)) ⊆ ℝ → (((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ SConn ↔ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))))
55	50, 54	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ SConn ↔ ∀𝑢 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))∀𝑣 ∈ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))(𝑢[,]𝑣) ⊆ ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵)))
56	49, 55	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ((topGen‘ran (,)) ↾t ((𝑎(,)𝑏) ∩ (𝐴[,]𝐵))) ∈ SConn)
57	17, 56	eqeltrd 2863	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn)
58	13, 14, 57	3jca 1146	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) ∧ (𝑧 = (𝑎(,)𝑏) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) → ((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))
59	58	exp32 426	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (𝑧 = (𝑎(,)𝑏) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))))
60	59	rexlimdvw 3171	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))))
61	60	rexlimdvw 3171	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))))
62	10, 61	biimtrid 245	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (𝑧 ∈ ran (,) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))))
63	62	reximdvai 3176	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (∃𝑧 ∈ ran (,)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ∃𝑧 ∈ ran (,)((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn)))
64		retopbas 25091	. . . . . 6 ⊢ ran (,) ∈ TopBases
65		bastg 23296	. . . . . 6 ⊢ (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
66		ssrexv 3982	. . . . . 6 ⊢ (ran (,) ⊆ (topGen‘ran (,)) → (∃𝑧 ∈ ran (,)((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn) → ∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn)))
67	64, 65, 66	mp2b 10	. . . . 5 ⊢ (∃𝑧 ∈ ran (,)((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn) → ∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))
68	63, 67	syl6 36	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → (∃𝑧 ∈ ran (,)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥) → ∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn)))
69	6, 68	mpd 16	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑥 ∈ (topGen‘ran (,)) ∧ 𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵)))) → ∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))
70	69	ralrimivva 3208	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ (topGen‘ran (,))∀𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵))∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))
71		retop 25092	. . 3 ⊢ (topGen‘ran (,)) ∈ Top
72		ovex 7460	. . 3 ⊢ (𝐴[,]𝐵) ∈ V
73		subislly 23812	. . 3 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) → (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn ↔ ∀𝑥 ∈ (topGen‘ran (,))∀𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵))∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn)))
74	71, 72, 73	mp2an 705	. 2 ⊢ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn ↔ ∀𝑥 ∈ (topGen‘ran (,))∀𝑦 ∈ (𝑥 ∩ (𝐴[,]𝐵))∃𝑧 ∈ (topGen‘ran (,))((𝑧 ∩ (𝐴[,]𝐵)) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ((topGen‘ran (,)) ↾t (𝑧 ∩ (𝐴[,]𝐵))) ∈ SConn))
75	70, 74	sylibr 237	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  ∀wral 3079  ∃wrex 3089  Vcvv 3453   ⊆ wss 3899   ∩ cin 4091  𝒫 cpw 4559   × cxp 5652  ran crn 5655   Fn wfn 6541  ⟶wf 6542  ‘cfv 6546  (class class class)co 7427  ℝcr 11209  ℝ^*cxr 11352  (,)cioo 13486  [,]cicc 13489   ↾_t crest 17603  topGenctg 17620  Topctop 23223  TopBasesctb 23275  Conncconn 23741  Locally clly 23795  SConncsconn 36106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287  ax-pre-sup 11288  ax-addf 11289

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4838  df-uni 4870  df-int 4910  df-iun 4955  df-iin 4956  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-se 5608  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-of 7700  df-om 7885  df-1st 8008  df-2nd 8009  df-supp 8188  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-2o 8488  df-er 8728  df-map 8860  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9365  df-fi 9413  df-sup 9444  df-inf 9445  df-oi 9514  df-card 10030  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-div 11984  df-nn 12346  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422  df-n0 12617  df-z 12704  df-dec 12825  df-uz 12976  df-q 13086  df-rp 13131  df-xneg 13251  df-xadd 13252  df-xmul 13253  df-ioo 13490  df-ico 13492  df-icc 13493  df-fz 13650  df-fzo 13799  df-seq 14155  df-exp 14215  df-hash 14485  df-cj 15278  df-re 15279  df-im 15280  df-sqrt 15414  df-abs 15415  df-struct 17337  df-sets 17354  df-slot 17372  df-ndx 17384  df-base 17400  df-ress 17421  df-plusg 17453  df-mulr 17454  df-starv 17455  df-sca 17456  df-vsca 17457  df-ip 17458  df-tset 17459  df-ple 17460  df-ds 17462  df-unif 17463  df-hom 17464  df-cco 17465  df-rest 17605  df-topn 17606  df-0g 17624  df-gsum 17625  df-topgen 17626  df-pt 17627  df-prds 17630  df-xrs 17686  df-qtop 17691  df-imas 17692  df-xps 17694  df-mre 17768  df-mrc 17769  df-acs 17771  df-mgm 18828  df-sgrp 18920  df-mnd 18936  df-submnd 18991  df-mulg 19290  df-cntz 19543  df-cmn 20008  df-psmet 21682  df-xmet 21683  df-met 21684  df-bl 21685  df-mopn 21686  df-cnfld 21691  df-top 23224  df-topon 23241  df-topsp 23263  df-bases 23276  df-cld 23349  df-cn 23557  df-cnp 23558  df-conn 23742  df-lly 23797  df-tx 23893  df-hmeo 24086  df-xms 24651  df-ms 24652  df-tms 24653  df-ii 25210  df-cncf 25211  df-htpy 25303  df-phtpy 25304  df-phtpc 25325  df-pconn 36107  df-sconn 36108

This theorem is used by:  iillysconn  36139