Theorem relowlpssretop 33212

Description: The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.)

Hypothesis

Ref	Expression
relowlpssretop.1	⊢ 𝐼 = ([,) “ (ℝ × ℝ))

Assertion

Ref	Expression
relowlpssretop	⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Proof of Theorem relowlpssretop

Dummy variables 𝑎 𝑏 𝑐 𝑖 𝑜 𝑥 𝑚 𝑛 𝑧 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relowlpssretop.1	. . 3 ⊢ 𝐼 = ([,) “ (ℝ × ℝ))
2	1	relowlssretop 33211	. 2 ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
3		2re 11090	. . . . 5 ⊢ 2 ∈ ℝ
4		1lt2 11194	. . . . 5 ⊢ 1 < 2
5		ovex 6678	. . . . . . . . . . . 12 ⊢ (1[,)𝑐) ∈ V
6		sbcan 3478	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ ([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐))
7		1re 10039	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
8		sbcg 3503	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ)
10		sbcbr123 4706	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ ⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐)
11		csbvarg 4003	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑥 = 1)
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑥 = 1
13		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑐 = 𝑐)
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑐 = 𝑐
15	12, 14	breq12i 4662	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐 ↔ 1⦋1 / 𝑥⦌ < 𝑐)
16		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌ < = < )
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌ < = <
18	17	breqi 4659	. . . . . . . . . . . . . . . . 17 ⊢ (1⦋1 / 𝑥⦌ < 𝑐 ↔ 1 < 𝑐)
19	10, 15, 18	3bitri 286	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ 1 < 𝑐)
20	9, 19	anbi12i 733	. . . . . . . . . . . . . . 15 ⊢ (([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
21	6, 20	bitri 264	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
22		sbceqg 3984	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐)))
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐))
24		csbconstg 3546	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑖 = 𝑖)
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌𝑖 = 𝑖
26		csbov123 6687	. . . . . . . . . . . . . . . . 17 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐)
27		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌[,) = [,))
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌[,) = [,)
29	12, 14, 28	oveq123i 6664	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐) = (1[,)𝑐)
30	26, 29	eqtri 2644	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (1[,)𝑐)
31	25, 30	eqeq12i 2636	. . . . . . . . . . . . . . 15 ⊢ (⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
32	23, 31	bitri 264	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
33		sbcan 3478	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ↔ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)))
34		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑥 ∈ ℝ)
36		leid 10133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ 𝑥)
37	35, 36	jccir 562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥))
38		rexr 10085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 ∈ ℝ → 𝑐 ∈ ℝ*)
39		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
40	38, 39	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
41		df-3an 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐))
42	40, 41	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐)))
43	42	baibd 948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥)) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
44	37, 43	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
45	44	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) → 𝑥 ∈ (𝑥[,)𝑐))
46	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ (𝑥[,)𝑐))
47		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
48	47	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
49	46, 48	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ 𝑖)
50		rexpssxrxp 10084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
51		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ))
52	50, 51	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
53		df-ico 12181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑐 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐)})
54	53	ixxf 12185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
55	54	fdmi 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ dom [,) = (ℝ* × ℝ*)
56	55	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) ↔ ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
57	53	mpt2fun 6762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Fun [,)
58		funfvima 6492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((Fun [,) ∧ ⟨𝑥, 𝑐⟩ ∈ dom [,)) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
59	57, 58	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
60	56, 59	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
61	52, 51, 60	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ)))
62		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥[,)𝑐) = ([,)‘⟨𝑥, 𝑐⟩)
63	61, 62, 1	3eltr4g 2718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥[,)𝑐) ∈ 𝐼)
64		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑖 ∈ 𝐼 ↔ (𝑥[,)𝑐) ∈ 𝐼))
65	63, 64	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑖 = (𝑥[,)𝑐) → 𝑖 ∈ 𝐼))
66	65	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑖 ∈ 𝐼)
67		ioof 12271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
68		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (,) Fn (ℝ* × ℝ*)
70		ovelrn 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
72		iooelexlt 33210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥)
73		df-rex 2918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥 ↔ ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
74	72, 73	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
75		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏)))
77	53	elmpt2cl2 6878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑦 ∈ (𝑥[,)𝑐) → 𝑐 ∈ ℝ*)
78		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
79		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
80	78, 79	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
81		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐) → 𝑥 ≤ 𝑦)
82	80, 81	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
83	82	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑐 ∈ ℝ* → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦)))
84	83	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → (𝑐 ∈ ℝ* → 𝑥 ≤ 𝑦)))
85	77, 84	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
86	85	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ≤ 𝑦)
87	78	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ*)
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ∈ ℝ*)
89		elicore 12226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
90	78, 89	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
91	90	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ*)
92		xrlenlt 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥))
93	92	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 → ¬ 𝑦 < 𝑥))
94	93	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
95	88, 91, 94	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
96	86, 95	mt2d 131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ 𝑦 < 𝑥)
97	96	intnand 962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
98	97	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥)))
99	98	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ 𝑦 ∈ (𝑥[,)𝑐)))
100	76, 99	jcad 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → (𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐))))
101		annim 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
102	100, 101	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
103	102	eximdv 1846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
105		exnal 1754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
106	104, 105	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
107		dfss2 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎(,)𝑏) ⊆ (𝑥[,)𝑐) ↔ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
108	106, 107	sylnibr 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
109		imnan 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)) ↔ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
110	108, 109	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
111		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
112		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑜 ⊆ (𝑥[,)𝑐) ↔ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
113	111, 112	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))))
114	110, 113	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑜 = (𝑎(,)𝑏) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)))
115		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ (𝑥[,)𝑐)))
116	115	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = (𝑥[,)𝑐) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
117	116	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = (𝑥[,)𝑐) → (¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
118	114, 117	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
120	119	rexlimivv 3036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
121	71, 120	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑜 ∈ ran (,) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ∈ ran (,) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
123	122	ralrimiv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → ∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
124		ralnex 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
125	123, 124	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (𝑥[,)𝑐) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
126	125	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
127	66, 126	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
128	127	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
129	49, 128	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
130		an12 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
131		annim 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
132	131	anbi2i 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
133	130, 132	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
134	129, 133	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
135		rspe 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
137		rexnal 2995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
138	136, 137	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
139	138	exp41 638	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
140	139	com4l 92	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ ℝ → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
141	140	imp41 619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
142		rspe 3003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
143	34, 141, 142	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
144		rexnal 2995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
145	143, 144	sylib 208	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
146		df-ico 12181	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ [,) = (𝑚 ∈ ℝ*, 𝑛 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛)})
147	146	ixxex 12186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ [,) ∈ V
148		imaexg 7103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([,) ∈ V → ([,) “ (ℝ × ℝ)) ∈ V)
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([,) “ (ℝ × ℝ)) ∈ V
150	1, 149	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 ∈ V
151	1	icoreunrn 33207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ 𝐼
152		unirnioo 12273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ ran (,)
153	151, 152	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝐼 = ∪ ran (,)
154		tgss2 20791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,)) → ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
155	150, 153, 154	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
156	151	raleqi 3142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
157	155, 156	bitr4i 267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
158	145, 157	sylnibr 319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
159	158	sbcth 3450	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
161		sbcimg 3477	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → ([1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → [1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))))
162	7, 161	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → [1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
163	160, 162	mpbi 220	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → [1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
164		sbcel1v 3495	. . . . . . . . . . . . . . . . . 18 ⊢ ([1 / 𝑥]𝑥 ∈ ℝ ↔ 1 ∈ ℝ)
165	7, 164	mpbir 221	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]𝑥 ∈ ℝ
166		sbcan 3478	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ [1 / 𝑥]𝑥 ∈ ℝ))
167	165, 166	mpbiran2 954	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ [1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)))
168		sbcg 3503	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
169	7, 168	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
170	163, 167, 169	3imtr3i 280	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
171	33, 170	sylbir 225	. . . . . . . . . . . . . 14 ⊢ (([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
172	21, 32, 171	syl2anbr 497	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
173	172	sbcth 3450	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
174	5, 173	ax-mp 5	. . . . . . . . . . 11 ⊢ [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
175		sbcimg 3477	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → [(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))))
176	5, 175	ax-mp 5	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → [(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
177	174, 176	mpbi 220	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → [(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
178		sbcan 3478	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
179		eqid 2622	. . . . . . . . . . . . 13 ⊢ (1[,)𝑐) = (1[,)𝑐)
180		eqsbc3 3475	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐)))
181	5, 180	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐))
182	179, 181	mpbir 221	. . . . . . . . . . . 12 ⊢ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)
183		sbcg 3503	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐)))
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
185	184	anbi1i 731	. . . . . . . . . . . 12 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
186	182, 185	mpbiran2 954	. . . . . . . . . . 11 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
187	178, 186	bitri 264	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
188		sbcg 3503	. . . . . . . . . . 11 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
189	5, 188	ax-mp 5	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
190	177, 187, 189	3imtr3i 280	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
191	190	sbcth 3450	. . . . . . . 8 ⊢ (2 ∈ ℝ → [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
192	3, 191	ax-mp 5	. . . . . . 7 ⊢ [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
193		sbcimg 3477	. . . . . . . 8 ⊢ (2 ∈ ℝ → ([2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) → [2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))))
194	3, 193	ax-mp 5	. . . . . . 7 ⊢ ([2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))) ↔ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) → [2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
195	192, 194	mpbi 220	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) → [2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
196		sbcan 3478	. . . . . . 7 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ ([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐))
197		sbcel1v 3495	. . . . . . . 8 ⊢ ([2 / 𝑐]𝑐 ∈ ℝ ↔ 2 ∈ ℝ)
198		sbcbr123 4706	. . . . . . . . 9 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ ⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐)
199		csbconstg 3546	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌1 = 1)
200	3, 199	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌1 = 1
201		csbvarg 4003	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌𝑐 = 2)
202	3, 201	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌𝑐 = 2
203	200, 202	breq12i 4662	. . . . . . . . 9 ⊢ (⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐 ↔ 1⦋2 / 𝑐⦌ < 2)
204		csbconstg 3546	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌ < = < )
205	3, 204	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌ < = <
206	205	breqi 4659	. . . . . . . . 9 ⊢ (1⦋2 / 𝑐⦌ < 2 ↔ 1 < 2)
207	198, 203, 206	3bitri 286	. . . . . . . 8 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ 1 < 2)
208	197, 207	anbi12i 733	. . . . . . 7 ⊢ (([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
209	196, 208	bitri 264	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
210		sbcg 3503	. . . . . . 7 ⊢ (2 ∈ ℝ → ([2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
211	3, 210	ax-mp 5	. . . . . 6 ⊢ ([2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
212	195, 209, 211	3imtr3i 280	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
213	3, 4, 212	mp2an 708	. . . 4 ⊢ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))
214		eqimss 3657	. . . 4 ⊢ ((topGen‘𝐼) = (topGen‘ran (,)) → (topGen‘𝐼) ⊆ (topGen‘ran (,)))
215	213, 214	mto 188	. . 3 ⊢ ¬ (topGen‘𝐼) = (topGen‘ran (,))
216	215	nesymir 2852	. 2 ⊢ (topGen‘ran (,)) ≠ (topGen‘𝐼)
217		df-pss 3590	. 2 ⊢ ((topGen‘ran (,)) ⊊ (topGen‘𝐼) ↔ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ∧ (topGen‘ran (,)) ≠ (topGen‘𝐼)))
218	2, 216, 217	mpbir2an 955	1 ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200  [wsbc 3435  ⦋csb 3533   ⊆ wss 3574   ⊊ wpss 3575  𝒫 cpw 4158  ⟨cop 4183  ∪ cuni 4436   class class class wbr 4653   × cxp 5112  dom cdm 5114  ran crn 5115   “ cima 5117  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  ℝcr 9935  1c1 9937  ℝ^*cxr 10073   < clt 10074   ≤ cle 10075  2c2 11070  (,)cioo 12175  [,)cico 12177  topGenctg 16098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-2 11079  df-ioo 12179  df-ico 12181  df-topgen 16104

This theorem is referenced by: (None)