Theorem relowlpssretop 36779

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 36778	. 2 ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
3		2re 12308	. . . . 5 ⊢ 2 ∈ ℝ
4		1lt2 12405	. . . . 5 ⊢ 1 < 2
5		ovex 7447	. . . . . . . . . . . 12 ⊢ (1[,)𝑐) ∈ V
6		sbcan 3826	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ ([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐))
7		1re 11236	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
8		sbcg 3852	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ)
10		sbcbr123 5196	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ ⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐)
11		csbvarg 4427	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑥 = 1)
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑥 = 1
13		csbconstg 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑐 = 𝑐)
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑐 = 𝑐
15	12, 14	breq12i 5151	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐 ↔ 1⦋1 / 𝑥⦌ < 𝑐)
16		csbconstg 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌ < = < )
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌ < = <
18	17	breqi 5148	. . . . . . . . . . . . . . . . 17 ⊢ (1⦋1 / 𝑥⦌ < 𝑐 ↔ 1 < 𝑐)
19	10, 15, 18	3bitri 297	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ 1 < 𝑐)
20	9, 19	anbi12i 626	. . . . . . . . . . . . . . 15 ⊢ (([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
21	6, 20	bitri 275	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
22		sbceqg 4405	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐)))
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐))
24		csbconstg 3908	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑖 = 𝑖)
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌𝑖 = 𝑖
26		csbov123 7456	. . . . . . . . . . . . . . . . 17 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐)
27		csbconstg 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌[,) = [,))
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌[,) = [,)
29	12, 14, 28	oveq123i 7428	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐) = (1[,)𝑐)
30	26, 29	eqtri 2755	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (1[,)𝑐)
31	25, 30	eqeq12i 2745	. . . . . . . . . . . . . . 15 ⊢ (⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
32	23, 31	bitri 275	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
33		sbcan 3826	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ↔ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)))
34		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑥 ∈ ℝ)
36		leid 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ 𝑥)
37	35, 36	jccir 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥))
38		rexr 11282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 ∈ ℝ → 𝑐 ∈ ℝ*)
39		elico2 13412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
40	38, 39	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
41		df-3an 1087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐))
42	40, 41	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐)))
43	42	baibd 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥)) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
44	37, 43	mpdan 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
45	44	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) → 𝑥 ∈ (𝑥[,)𝑐))
46	45	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ (𝑥[,)𝑐))
47		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
48	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
49	46, 48	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ 𝑖)
50		rexpssxrxp 11281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
51		opelxpi 5709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ))
52	50, 51	sselid 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
53		df-ico 13354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑐 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐)})
54	53	ixxf 13358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
55	54	fdmi 6728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ dom [,) = (ℝ* × ℝ*)
56	55	eleq2i 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) ↔ ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
57	53	mpofun 7538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Fun [,)
58		funfvima 7236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((Fun [,) ∧ ⟨𝑥, 𝑐⟩ ∈ dom [,)) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
59	57, 58	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
60	56, 59	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
61	52, 51, 60	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ)))
62		df-ov 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥[,)𝑐) = ([,)‘⟨𝑥, 𝑐⟩)
63	61, 62, 1	3eltr4g 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥[,)𝑐) ∈ 𝐼)
64		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑖 ∈ 𝐼 ↔ (𝑥[,)𝑐) ∈ 𝐼))
65	63, 64	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑖 = (𝑥[,)𝑐) → 𝑖 ∈ 𝐼))
66	65	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑖 ∈ 𝐼)
67		ioof 13448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
68		ffn 6716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (,) Fn (ℝ* × ℝ*)
70		ovelrn 7591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
72		iooelexlt 36777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥)
73		df-rex 3066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥 ↔ ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
75		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏)))
77	53	elmpocl2 7658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑦 ∈ (𝑥[,)𝑐) → 𝑐 ∈ ℝ*)
78		elioore 13378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
79		elico2 13412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
80	78, 79	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
81		simp2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐) → 𝑥 ≤ 𝑦)
82	80, 81	biimtrdi 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 11286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ*)
88	87	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ∈ ℝ*)
89		elicore 13400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
90	78, 89	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
91	90	rexrd 11286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ*)
92		xrlenlt 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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	imbitrdi 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
103	102	eximdv 1913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
105		exnal 1822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
106	104, 105	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
107		dfss2 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎(,)𝑏) ⊆ (𝑥[,)𝑐) ↔ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
108	106, 107	sylnibr 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
109		imnan 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)) ↔ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
110	108, 109	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
111		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
112		sseq1 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑜 ⊆ (𝑥[,)𝑐) ↔ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
113	111, 112	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))))
114	110, 113	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑜 = (𝑎(,)𝑏) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)))
115		sseq2 4004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ (𝑥[,)𝑐)))
116	115	anbi2d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = (𝑥[,)𝑐) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
117	116	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = (𝑥[,)𝑐) → (¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
118	114, 117	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
120	119	rexlimivv 3194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
121	71, 120	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑜 ∈ ran (,) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ∈ ran (,) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
123	122	ralrimiv 3140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → ∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
124		ralnex 3067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
129	49, 128	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
130		an12 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
131		annim 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
132	131	anbi2i 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
133	130, 132	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
134	129, 133	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
135		rspe 3241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
137		rexnal 3095	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
143	34, 141, 142	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
144		rexnal 3095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
145	143, 144	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
146		df-ico 13354	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ [,) = (𝑚 ∈ ℝ*, 𝑛 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛)})
147	146	ixxex 13359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ [,) ∈ V
148		imaexg 7915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([,) ∈ V → ([,) “ (ℝ × ℝ)) ∈ V)
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([,) “ (ℝ × ℝ)) ∈ V
150	1, 149	eqeltri 2824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 ∈ V
151	1	icoreunrn 36774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ 𝐼
152		unirnioo 13450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ ran (,)
153	151, 152	eqtr3i 2757	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝐼 = ∪ ran (,)
154		tgss2 22877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,)) → ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
155	150, 153, 154	mp2an 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
156	151	raleqi 3318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
157	155, 156	bitr4i 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
158	145, 157	sylnibr 329	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
159	158	sbcth 3789	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
161		sbcimg 3825	. . . . . . . . . . . . . . . . . 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 3844	. . . . . . . . . . . . . . . . . 18 ⊢ ([1 / 𝑥]𝑥 ∈ ℝ ↔ 1 ∈ ℝ)
165	7, 164	mpbir 230	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]𝑥 ∈ ℝ
166		sbcan 3826	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ [1 / 𝑥]𝑥 ∈ ℝ))
167	165, 166	mpbiran2 709	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ [1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)))
168		sbcg 3852	. . . . . . . . . . . . . . . . 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 291	. . . . . . . . . . . . . . 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 3789	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
174	5, 173	ax-mp 5	. . . . . . . . . . 11 ⊢ [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
175		sbcimg 3825	. . . . . . . . . . . 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 3826	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
179		eqid 2727	. . . . . . . . . . . . 13 ⊢ (1[,)𝑐) = (1[,)𝑐)
180		eqsbc1 3823	. . . . . . . . . . . . . 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 3852	. . . . . . . . . . . . . 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 709	. . . . . . . . . . 11 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
187	178, 186	bitri 275	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
188		sbcg 3852	. . . . . . . . . . 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 291	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
191	190	sbcth 3789	. . . . . . . 8 ⊢ (2 ∈ ℝ → [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
192	3, 191	ax-mp 5	. . . . . . 7 ⊢ [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
193		sbcimg 3825	. . . . . . . 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 3826	. . . . . . 7 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ ([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐))
197		sbcel1v 3844	. . . . . . . 8 ⊢ ([2 / 𝑐]𝑐 ∈ ℝ ↔ 2 ∈ ℝ)
198		sbcbr123 5196	. . . . . . . . 9 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ ⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐)
199		csbconstg 3908	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌1 = 1)
200	3, 199	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌1 = 1
201		csbvarg 4427	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌𝑐 = 2)
202	3, 201	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌𝑐 = 2
203	200, 202	breq12i 5151	. . . . . . . . 9 ⊢ (⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐 ↔ 1⦋2 / 𝑐⦌ < 2)
204		csbconstg 3908	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌ < = < )
205	3, 204	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌ < = <
206	205	breqi 5148	. . . . . . . . 9 ⊢ (1⦋2 / 𝑐⦌ < 2 ↔ 1 < 2)
207	198, 203, 206	3bitri 297	. . . . . . . 8 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ 1 < 2)
208	197, 207	anbi12i 626	. . . . . . 7 ⊢ (([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
209	196, 208	bitri 275	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
210		sbcg 3852	. . . . . . 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 291	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
213	3, 4, 212	mp2an 691	. . . 4 ⊢ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))
214		eqimss 4036	. . . 4 ⊢ ((topGen‘𝐼) = (topGen‘ran (,)) → (topGen‘𝐼) ⊆ (topGen‘ran (,)))
215	213, 214	mto 196	. . 3 ⊢ ¬ (topGen‘𝐼) = (topGen‘ran (,))
216	215	nesymir 2994	. 2 ⊢ (topGen‘ran (,)) ≠ (topGen‘𝐼)
217		df-pss 3963	. 2 ⊢ ((topGen‘ran (,)) ⊊ (topGen‘𝐼) ↔ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ∧ (topGen‘ran (,)) ≠ (topGen‘𝐼)))
218	2, 216, 217	mpbir2an 710	1 ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2935  ∀wral 3056  ∃wrex 3065  {crab 3427  Vcvv 3469  [wsbc 3774  ⦋csb 3889   ⊆ wss 3944   ⊊ wpss 3945  𝒫 cpw 4598  ⟨cop 4630  ∪ cuni 4903   class class class wbr 5142   × cxp 5670  dom cdm 5672  ran crn 5673   “ cima 5675  Fun wfun 6536   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7414  ℝcr 11129  1c1 11131  ℝ^*cxr 11269   < clt 11270   ≤ cle 11271  2c2 12289  (,)cioo 13348  [,)cico 13350  topGenctg 17410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-2 12297  df-ioo 13352  df-ico 13354  df-topgen 17416

This theorem is referenced by: (None)