Theorem relowlpssretop 35563

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 35562	. 2 ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
3		2re 12075	. . . . 5 ⊢ 2 ∈ ℝ
4		1lt2 12172	. . . . 5 ⊢ 1 < 2
5		ovex 7328	. . . . . . . . . . . 12 ⊢ (1[,)𝑐) ∈ V
6		sbcan 3770	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ ([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐))
7		1re 11003	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
8		sbcg 3797	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ)
10		sbcbr123 5131	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ ⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐)
11		csbvarg 4368	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑥 = 1)
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑥 = 1
13		csbconstg 3853	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑐 = 𝑐)
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑐 = 𝑐
15	12, 14	breq12i 5086	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐 ↔ 1⦋1 / 𝑥⦌ < 𝑐)
16		csbconstg 3853	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌ < = < )
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌ < = <
18	17	breqi 5083	. . . . . . . . . . . . . . . . 17 ⊢ (1⦋1 / 𝑥⦌ < 𝑐 ↔ 1 < 𝑐)
19	10, 15, 18	3bitri 296	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ 1 < 𝑐)
20	9, 19	anbi12i 626	. . . . . . . . . . . . . . 15 ⊢ (([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
21	6, 20	bitri 274	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
22		sbceqg 4346	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐)))
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐))
24		csbconstg 3853	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑖 = 𝑖)
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌𝑖 = 𝑖
26		csbov123 7337	. . . . . . . . . . . . . . . . 17 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐)
27		csbconstg 3853	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌[,) = [,))
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌[,) = [,)
29	12, 14, 28	oveq123i 7309	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐) = (1[,)𝑐)
30	26, 29	eqtri 2761	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (1[,)𝑐)
31	25, 30	eqeq12i 2751	. . . . . . . . . . . . . . 15 ⊢ (⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
32	23, 31	bitri 274	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
33		sbcan 3770	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ↔ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)))
34		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑥 ∈ ℝ)
36		leid 11099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ 𝑥)
37	35, 36	jccir 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥))
38		rexr 11049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 ∈ ℝ → 𝑐 ∈ ℝ*)
39		elico2 13171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
40	38, 39	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
41		df-3an 1087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐))
42	40, 41	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐)))
43	42	baibd 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥)) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
44	37, 43	mpdan 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
45	44	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) → 𝑥 ∈ (𝑥[,)𝑐))
46	45	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ (𝑥[,)𝑐))
47		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
48	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
49	46, 48	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ 𝑖)
50		rexpssxrxp 11048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
51		opelxpi 5628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ))
52	50, 51	sselid 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
53		df-ico 13113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑐 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐)})
54	53	ixxf 13117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
55	54	fdmi 6630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ dom [,) = (ℝ* × ℝ*)
56	55	eleq2i 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) ↔ ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
57	53	mpofun 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Fun [,)
58		funfvima 7126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((Fun [,) ∧ ⟨𝑥, 𝑐⟩ ∈ dom [,)) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
59	57, 58	mpan 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
60	56, 59	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
61	52, 51, 60	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ)))
62		df-ov 7298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥[,)𝑐) = ([,)‘⟨𝑥, 𝑐⟩)
63	61, 62, 1	3eltr4g 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥[,)𝑐) ∈ 𝐼)
64		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑖 ∈ 𝐼 ↔ (𝑥[,)𝑐) ∈ 𝐼))
65	63, 64	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑖 = (𝑥[,)𝑐) → 𝑖 ∈ 𝐼))
66	65	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑖 ∈ 𝐼)
67		ioof 13207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
68		ffn 6618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (,) Fn (ℝ* × ℝ*)
70		ovelrn 7468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
72		iooelexlt 35561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥)
73		df-rex 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥 ↔ ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
75		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏)))
77	53	elmpocl2 7533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑦 ∈ (𝑥[,)𝑐) → 𝑐 ∈ ℝ*)
78		elioore 13137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
79		elico2 13171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
80	78, 79	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
81		simp2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐) → 𝑥 ≤ 𝑦)
82	80, 81	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
83	82	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑐 ∈ ℝ* → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦)))
84	83	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → (𝑐 ∈ ℝ* → 𝑥 ≤ 𝑦)))
85	77, 84	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
86	85	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ≤ 𝑦)
87	78	rexrd 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ*)
88	87	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ∈ ℝ*)
89		elicore 13159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
90	78, 89	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
91	90	rexrd 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ*)
92		xrlenlt 11068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥))
93	92	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 → ¬ 𝑦 < 𝑥))
94	93	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
95	88, 91, 94	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
96	86, 95	mt2d 136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ 𝑦 < 𝑥)
97	96	intnand 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
98	97	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥)))
99	98	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ 𝑦 ∈ (𝑥[,)𝑐)))
100	76, 99	jcad 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → (𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐))))
101		annim 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
102	100, 101	syl6ib 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
103	102	eximdv 1916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
105		exnal 1825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
106	104, 105	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
107		dfss2 3909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎(,)𝑏) ⊆ (𝑥[,)𝑐) ↔ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
108	106, 107	sylnibr 328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
109		imnan 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)) ↔ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
110	108, 109	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
111		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
112		sseq1 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑜 ⊆ (𝑥[,)𝑐) ↔ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
113	111, 112	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))))
114	110, 113	mtbiri 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑜 = (𝑎(,)𝑏) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)))
115		sseq2 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ (𝑥[,)𝑐)))
116	115	anbi2d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = (𝑥[,)𝑐) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
117	116	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = (𝑥[,)𝑐) → (¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
118	114, 117	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
120	119	rexlimivv 3190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
121	71, 120	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑜 ∈ ran (,) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ∈ ran (,) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
123	122	ralrimiv 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → ∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
124		ralnex 3070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
125	123, 124	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (𝑥[,)𝑐) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
126	125	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
127	66, 126	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
128	127	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
129	49, 128	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
130		an12 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
131		annim 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
132	131	anbi2i 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
133	130, 132	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
134	129, 133	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
135		rspe 3265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
137		rexnal 3097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
139	138	exp41 434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
140	139	com4l 92	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ ℝ → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
141	140	imp41 425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
142		rspe 3265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
143	34, 141, 142	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
144		rexnal 3097	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
145	143, 144	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
146		df-ico 13113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ [,) = (𝑚 ∈ ℝ*, 𝑛 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛)})
147	146	ixxex 13118	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ [,) ∈ V
148		imaexg 7782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([,) ∈ V → ([,) “ (ℝ × ℝ)) ∈ V)
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([,) “ (ℝ × ℝ)) ∈ V
150	1, 149	eqeltri 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 ∈ V
151	1	icoreunrn 35558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ 𝐼
152		unirnioo 13209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ ran (,)
153	151, 152	eqtr3i 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝐼 = ∪ ran (,)
154		tgss2 22165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,)) → ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
155	150, 153, 154	mp2an 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
156	151	raleqi 3348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
157	155, 156	bitr4i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
158	145, 157	sylnibr 328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
159	158	sbcth 3733	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
161		sbcimg 3769	. . . . . . . . . . . . . . . . . 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 229	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → [1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
164		sbcel1v 3789	. . . . . . . . . . . . . . . . . 18 ⊢ ([1 / 𝑥]𝑥 ∈ ℝ ↔ 1 ∈ ℝ)
165	7, 164	mpbir 230	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]𝑥 ∈ ℝ
166		sbcan 3770	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ [1 / 𝑥]𝑥 ∈ ℝ))
167	165, 166	mpbiran2 706	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ [1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)))
168		sbcg 3797	. . . . . . . . . . . . . . . . 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 290	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
171	33, 170	sylbir 234	. . . . . . . . . . . . . 14 ⊢ (([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
172	21, 32, 171	syl2anbr 598	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
173	172	sbcth 3733	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
174	5, 173	ax-mp 5	. . . . . . . . . . 11 ⊢ [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
175		sbcimg 3769	. . . . . . . . . . . 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 229	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → [(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
178		sbcan 3770	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
179		eqid 2733	. . . . . . . . . . . . 13 ⊢ (1[,)𝑐) = (1[,)𝑐)
180		eqsbc1 3767	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐)))
181	5, 180	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐))
182	179, 181	mpbir 230	. . . . . . . . . . . 12 ⊢ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)
183		sbcg 3797	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐)))
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
185	184	anbi1i 623	. . . . . . . . . . . 12 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
186	182, 185	mpbiran2 706	. . . . . . . . . . 11 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
187	178, 186	bitri 274	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
188		sbcg 3797	. . . . . . . . . . 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 290	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
191	190	sbcth 3733	. . . . . . . 8 ⊢ (2 ∈ ℝ → [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
192	3, 191	ax-mp 5	. . . . . . 7 ⊢ [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
193		sbcimg 3769	. . . . . . . 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 229	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) → [2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
196		sbcan 3770	. . . . . . 7 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ ([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐))
197		sbcel1v 3789	. . . . . . . 8 ⊢ ([2 / 𝑐]𝑐 ∈ ℝ ↔ 2 ∈ ℝ)
198		sbcbr123 5131	. . . . . . . . 9 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ ⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐)
199		csbconstg 3853	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌1 = 1)
200	3, 199	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌1 = 1
201		csbvarg 4368	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌𝑐 = 2)
202	3, 201	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌𝑐 = 2
203	200, 202	breq12i 5086	. . . . . . . . 9 ⊢ (⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐 ↔ 1⦋2 / 𝑐⦌ < 2)
204		csbconstg 3853	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌ < = < )
205	3, 204	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌ < = <
206	205	breqi 5083	. . . . . . . . 9 ⊢ (1⦋2 / 𝑐⦌ < 2 ↔ 1 < 2)
207	198, 203, 206	3bitri 296	. . . . . . . 8 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ 1 < 2)
208	197, 207	anbi12i 626	. . . . . . 7 ⊢ (([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
209	196, 208	bitri 274	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
210		sbcg 3797	. . . . . . 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 290	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
213	3, 4, 212	mp2an 688	. . . 4 ⊢ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))
214		eqimss 3979	. . . 4 ⊢ ((topGen‘𝐼) = (topGen‘ran (,)) → (topGen‘𝐼) ⊆ (topGen‘ran (,)))
215	213, 214	mto 196	. . 3 ⊢ ¬ (topGen‘𝐼) = (topGen‘ran (,))
216	215	nesymir 2997	. 2 ⊢ (topGen‘ran (,)) ≠ (topGen‘𝐼)
217		df-pss 3908	. 2 ⊢ ((topGen‘ran (,)) ⊊ (topGen‘𝐼) ↔ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ∧ (topGen‘ran (,)) ≠ (topGen‘𝐼)))
218	2, 216, 217	mpbir2an 707	1 ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2101   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3221  Vcvv 3434  [wsbc 3718  ⦋csb 3834   ⊆ wss 3889   ⊊ wpss 3890  𝒫 cpw 4536  ⟨cop 4570  ∪ cuni 4841   class class class wbr 5077   × cxp 5589  dom cdm 5591  ran crn 5592   “ cima 5594  Fun wfun 6441   Fn wfn 6442  ⟶wf 6443  ‘cfv 6447  (class class class)co 7295  ℝcr 10898  1c1 10900  ℝ^*cxr 11036   < clt 11037   ≤ cle 11038  2c2 12056  (,)cioo 13107  [,)cico 13109  topGenctg 17176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608  ax-cnex 10955  ax-resscn 10956  ax-1cn 10957  ax-icn 10958  ax-addcl 10959  ax-addrcl 10960  ax-mulcl 10961  ax-mulrcl 10962  ax-mulcom 10963  ax-addass 10964  ax-mulass 10965  ax-distr 10966  ax-i2m1 10967  ax-1ne0 10968  ax-1rid 10969  ax-rnegex 10970  ax-rrecex 10971  ax-cnre 10972  ax-pre-lttri 10973  ax-pre-lttrn 10974  ax-pre-ltadd 10975  ax-pre-mulgt0 10976

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3222  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3908  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-po 5505  df-so 5506  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-riota 7252  df-ov 7298  df-oprab 7299  df-mpo 7300  df-1st 7851  df-2nd 7852  df-er 8518  df-en 8754  df-dom 8755  df-sdom 8756  df-pnf 11039  df-mnf 11040  df-xr 11041  df-ltxr 11042  df-le 11043  df-sub 11235  df-neg 11236  df-div 11661  df-2 12064  df-ioo 13111  df-ico 13113  df-topgen 17182

This theorem is referenced by: (None)