Theorem relowlpssretop 36240

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 36239	. 2 ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
3		2re 12285	. . . . 5 ⊢ 2 ∈ ℝ
4		1lt2 12382	. . . . 5 ⊢ 1 < 2
5		ovex 7441	. . . . . . . . . . . 12 ⊢ (1[,)𝑐) ∈ V
6		sbcan 3829	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ ([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐))
7		1re 11213	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
8		sbcg 3856	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ)
10		sbcbr123 5202	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ ⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐)
11		csbvarg 4431	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑥 = 1)
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑥 = 1
13		csbconstg 3912	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑐 = 𝑐)
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑐 = 𝑐
15	12, 14	breq12i 5157	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐 ↔ 1⦋1 / 𝑥⦌ < 𝑐)
16		csbconstg 3912	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌ < = < )
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌ < = <
18	17	breqi 5154	. . . . . . . . . . . . . . . . 17 ⊢ (1⦋1 / 𝑥⦌ < 𝑐 ↔ 1 < 𝑐)
19	10, 15, 18	3bitri 296	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ 1 < 𝑐)
20	9, 19	anbi12i 627	. . . . . . . . . . . . . . 15 ⊢ (([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
21	6, 20	bitri 274	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
22		sbceqg 4409	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐)))
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐))
24		csbconstg 3912	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑖 = 𝑖)
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌𝑖 = 𝑖
26		csbov123 7450	. . . . . . . . . . . . . . . . 17 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐)
27		csbconstg 3912	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌[,) = [,))
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌[,) = [,)
29	12, 14, 28	oveq123i 7422	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐) = (1[,)𝑐)
30	26, 29	eqtri 2760	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (1[,)𝑐)
31	25, 30	eqeq12i 2750	. . . . . . . . . . . . . . 15 ⊢ (⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
32	23, 31	bitri 274	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
33		sbcan 3829	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ↔ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)))
34		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑥 ∈ ℝ)
36		leid 11309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ 𝑥)
37	35, 36	jccir 522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥))
38		rexr 11259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 ∈ ℝ → 𝑐 ∈ ℝ*)
39		elico2 13387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
40	38, 39	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
41		df-3an 1089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐))
42	40, 41	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐)))
43	42	baibd 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥)) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
44	37, 43	mpdan 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
45	44	biimpar 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) → 𝑥 ∈ (𝑥[,)𝑐))
46	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ (𝑥[,)𝑐))
47		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
48	47	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
49	46, 48	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ 𝑖)
50		rexpssxrxp 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
51		opelxpi 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ))
52	50, 51	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
53		df-ico 13329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑐 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐)})
54	53	ixxf 13333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
55	54	fdmi 6729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ dom [,) = (ℝ* × ℝ*)
56	55	eleq2i 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) ↔ ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
57	53	mpofun 7531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Fun [,)
58		funfvima 7231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((Fun [,) ∧ ⟨𝑥, 𝑐⟩ ∈ dom [,)) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
59	57, 58	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
60	56, 59	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
61	52, 51, 60	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ)))
62		df-ov 7411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥[,)𝑐) = ([,)‘⟨𝑥, 𝑐⟩)
63	61, 62, 1	3eltr4g 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥[,)𝑐) ∈ 𝐼)
64		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑖 ∈ 𝐼 ↔ (𝑥[,)𝑐) ∈ 𝐼))
65	63, 64	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑖 = (𝑥[,)𝑐) → 𝑖 ∈ 𝐼))
66	65	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑖 ∈ 𝐼)
67		ioof 13423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
68		ffn 6717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (,) Fn (ℝ* × ℝ*)
70		ovelrn 7582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
72		iooelexlt 36238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥)
73		df-rex 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥 ↔ ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
75		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏)))
77	53	elmpocl2 7649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑦 ∈ (𝑥[,)𝑐) → 𝑐 ∈ ℝ*)
78		elioore 13353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
79		elico2 13387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
80	78, 79	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
81		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐) → 𝑥 ≤ 𝑦)
82	80, 81	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
83	82	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑐 ∈ ℝ* → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦)))
84	83	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → (𝑐 ∈ ℝ* → 𝑥 ≤ 𝑦)))
85	77, 84	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
86	85	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ≤ 𝑦)
87	78	rexrd 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ*)
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ∈ ℝ*)
89		elicore 13375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
90	78, 89	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
91	90	rexrd 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ*)
92		xrlenlt 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥))
93	92	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 → ¬ 𝑦 < 𝑥))
94	93	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
95	88, 91, 94	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
96	86, 95	mt2d 136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ 𝑦 < 𝑥)
97	96	intnand 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
98	97	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥)))
99	98	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ 𝑦 ∈ (𝑥[,)𝑐)))
100	76, 99	jcad 513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → (𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐))))
101		annim 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
102	100, 101	imbitrdi 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
103	102	eximdv 1920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
105		exnal 1829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
106	104, 105	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
107		dfss2 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎(,)𝑏) ⊆ (𝑥[,)𝑐) ↔ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
108	106, 107	sylnibr 328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
109		imnan 400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)) ↔ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
110	108, 109	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
111		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
112		sseq1 4007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑜 ⊆ (𝑥[,)𝑐) ↔ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
113	111, 112	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))))
114	110, 113	mtbiri 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑜 = (𝑎(,)𝑏) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)))
115		sseq2 4008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ (𝑥[,)𝑐)))
116	115	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = (𝑥[,)𝑐) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
117	116	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = (𝑥[,)𝑐) → (¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
118	114, 117	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
120	119	rexlimivv 3199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
121	71, 120	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑜 ∈ ran (,) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ∈ ran (,) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
123	122	ralrimiv 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → ∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
124		ralnex 3072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
125	123, 124	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (𝑥[,)𝑐) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
126	125	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
127	66, 126	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
128	127	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
129	49, 128	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
130		an12 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
131		annim 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
132	131	anbi2i 623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
133	130, 132	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
134	129, 133	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
135		rspe 3246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
137		rexnal 3100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
139	138	exp41 435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
140	139	com4l 92	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ ℝ → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
141	140	imp41 426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
142		rspe 3246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
143	34, 141, 142	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
144		rexnal 3100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
145	143, 144	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
146		df-ico 13329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ [,) = (𝑚 ∈ ℝ*, 𝑛 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛)})
147	146	ixxex 13334	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ [,) ∈ V
148		imaexg 7905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([,) ∈ V → ([,) “ (ℝ × ℝ)) ∈ V)
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([,) “ (ℝ × ℝ)) ∈ V
150	1, 149	eqeltri 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 ∈ V
151	1	icoreunrn 36235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ 𝐼
152		unirnioo 13425	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ ran (,)
153	151, 152	eqtr3i 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝐼 = ∪ ran (,)
154		tgss2 22489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,)) → ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
155	150, 153, 154	mp2an 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
156	151	raleqi 3323	. . . . . . . . . . . . . . . . . . . . 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 3792	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
161		sbcimg 3828	. . . . . . . . . . . . . . . . . 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 3848	. . . . . . . . . . . . . . . . . 18 ⊢ ([1 / 𝑥]𝑥 ∈ ℝ ↔ 1 ∈ ℝ)
165	7, 164	mpbir 230	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]𝑥 ∈ ℝ
166		sbcan 3829	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ [1 / 𝑥]𝑥 ∈ ℝ))
167	165, 166	mpbiran2 708	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ [1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)))
168		sbcg 3856	. . . . . . . . . . . . . . . . 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 599	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
173	172	sbcth 3792	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
174	5, 173	ax-mp 5	. . . . . . . . . . 11 ⊢ [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
175		sbcimg 3828	. . . . . . . . . . . 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 3829	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
179		eqid 2732	. . . . . . . . . . . . 13 ⊢ (1[,)𝑐) = (1[,)𝑐)
180		eqsbc1 3826	. . . . . . . . . . . . . 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 3856	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐)))
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
185	184	anbi1i 624	. . . . . . . . . . . 12 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
186	182, 185	mpbiran2 708	. . . . . . . . . . 11 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
187	178, 186	bitri 274	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
188		sbcg 3856	. . . . . . . . . . 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 3792	. . . . . . . 8 ⊢ (2 ∈ ℝ → [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
192	3, 191	ax-mp 5	. . . . . . 7 ⊢ [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
193		sbcimg 3828	. . . . . . . 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 3829	. . . . . . 7 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ ([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐))
197		sbcel1v 3848	. . . . . . . 8 ⊢ ([2 / 𝑐]𝑐 ∈ ℝ ↔ 2 ∈ ℝ)
198		sbcbr123 5202	. . . . . . . . 9 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ ⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐)
199		csbconstg 3912	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌1 = 1)
200	3, 199	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌1 = 1
201		csbvarg 4431	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌𝑐 = 2)
202	3, 201	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌𝑐 = 2
203	200, 202	breq12i 5157	. . . . . . . . 9 ⊢ (⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐 ↔ 1⦋2 / 𝑐⦌ < 2)
204		csbconstg 3912	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌ < = < )
205	3, 204	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌ < = <
206	205	breqi 5154	. . . . . . . . 9 ⊢ (1⦋2 / 𝑐⦌ < 2 ↔ 1 < 2)
207	198, 203, 206	3bitri 296	. . . . . . . 8 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ 1 < 2)
208	197, 207	anbi12i 627	. . . . . . 7 ⊢ (([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
209	196, 208	bitri 274	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
210		sbcg 3856	. . . . . . 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 690	. . . 4 ⊢ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))
214		eqimss 4040	. . . 4 ⊢ ((topGen‘𝐼) = (topGen‘ran (,)) → (topGen‘𝐼) ⊆ (topGen‘ran (,)))
215	213, 214	mto 196	. . 3 ⊢ ¬ (topGen‘𝐼) = (topGen‘ran (,))
216	215	nesymir 2999	. 2 ⊢ (topGen‘ran (,)) ≠ (topGen‘𝐼)
217		df-pss 3967	. 2 ⊢ ((topGen‘ran (,)) ⊊ (topGen‘𝐼) ↔ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ∧ (topGen‘ran (,)) ≠ (topGen‘𝐼)))
218	2, 216, 217	mpbir2an 709	1 ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3432  Vcvv 3474  [wsbc 3777  ⦋csb 3893   ⊆ wss 3948   ⊊ wpss 3949  𝒫 cpw 4602  ⟨cop 4634  ∪ cuni 4908   class class class wbr 5148   × cxp 5674  dom cdm 5676  ran crn 5677   “ cima 5679  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7408  ℝcr 11108  1c1 11110  ℝ^*cxr 11246   < clt 11247   ≤ cle 11248  2c2 12266  (,)cioo 13323  [,)cico 13325  topGenctg 17382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-2 12274  df-ioo 13327  df-ico 13329  df-topgen 17388

This theorem is referenced by: (None)