Theorem relowlpssretop 38038

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 38037	. 2 ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
3		2re 12321	. . . . 5 ⊢ 2 ∈ ℝ
4		1lt2 12419	. . . . 5 ⊢ 1 < 2
5		ovex 7445	. . . . . . . . . . . 12 ⊢ (1[,)𝑐) ∈ V
6		sbcan 3792	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ ([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐))
7		1re 11214	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
8		sbcg 3815	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ))
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ)
10		sbcbr123 5164	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ ⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐)
11		csbvarg 4398	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑥 = 1)
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑥 = 1
13		csbconstg 3871	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑐 = 𝑐)
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌𝑐 = 𝑐
15	12, 14	breq12i 5117	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌ < ⦋1 / 𝑥⦌𝑐 ↔ 1⦋1 / 𝑥⦌ < 𝑐)
16		csbconstg 3871	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌ < = < )
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌ < = <
18	17	breqi 5114	. . . . . . . . . . . . . . . . 17 ⊢ (1⦋1 / 𝑥⦌ < 𝑐 ↔ 1 < 𝑐)
19	10, 15, 18	3bitri 300	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥]𝑥 < 𝑐 ↔ 1 < 𝑐)
20	9, 19	anbi12i 639	. . . . . . . . . . . . . . 15 ⊢ (([1 / 𝑥]𝑐 ∈ ℝ ∧ [1 / 𝑥]𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
21	6, 20	bitri 278	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
22		sbceqg 4376	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐)))
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ ⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐))
24		csbconstg 3871	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌𝑖 = 𝑖)
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌𝑖 = 𝑖
26		csbov123 7456	. . . . . . . . . . . . . . . . 17 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐)
27		csbconstg 3871	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ⦋1 / 𝑥⦌[,) = [,))
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋1 / 𝑥⦌[,) = [,)
29	12, 14, 28	oveq123i 7426	. . . . . . . . . . . . . . . . 17 ⊢ (⦋1 / 𝑥⦌𝑥⦋1 / 𝑥⦌[,)⦋1 / 𝑥⦌𝑐) = (1[,)𝑐)
30	26, 29	eqtri 2785	. . . . . . . . . . . . . . . 16 ⊢ ⦋1 / 𝑥⦌(𝑥[,)𝑐) = (1[,)𝑐)
31	25, 30	eqeq12i 2780	. . . . . . . . . . . . . . 15 ⊢ (⦋1 / 𝑥⦌𝑖 = ⦋1 / 𝑥⦌(𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
32	23, 31	bitri 278	. . . . . . . . . . . . . 14 ⊢ ([1 / 𝑥]𝑖 = (𝑥[,)𝑐) ↔ 𝑖 = (1[,)𝑐))
33		sbcan 3792	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ↔ ([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)))
34		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑥 ∈ ℝ)
36		leid 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ 𝑥)
37	35, 36	jccir 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥))
38		rexr 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 ∈ ℝ → 𝑐 ∈ ℝ*)
39		elico2 13443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
40	38, 39	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐)))
41		df-3an 1104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐))
42	40, 41	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥) ∧ 𝑥 < 𝑐)))
43	42	baibd 548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ (𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥)) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
44	37, 43	mpdan 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑐) ↔ 𝑥 < 𝑐))
45	44	biimpar 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) → 𝑥 ∈ (𝑥[,)𝑐))
46	45	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ (𝑥[,)𝑐))
47		eleq2 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
48	47	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ (𝑥[,)𝑐)))
49	46, 48	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑥 ∈ 𝑖)
50		rexpssxrxp 11260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
51		opelxpi 5697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ))
52	50, 51	sselid 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
53		df-ico 13384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑐 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐)})
54	53	ixxf 13388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
55	54	fdmi 6717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ dom [,) = (ℝ* × ℝ*)
56	55	eleq2i 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) ↔ ⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*))
57	53	mpofun 7536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Fun [,)
58		funfvima 7228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((Fun [,) ∧ ⟨𝑥, 𝑐⟩ ∈ dom [,)) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
59	57, 58	mpan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑥, 𝑐⟩ ∈ dom [,) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
60	56, 59	sylbir 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑥, 𝑐⟩ ∈ (ℝ* × ℝ*) → (⟨𝑥, 𝑐⟩ ∈ (ℝ × ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ))))
61	52, 51, 60	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ([,)‘⟨𝑥, 𝑐⟩) ∈ ([,) “ (ℝ × ℝ)))
62		df-ov 7415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥[,)𝑐) = ([,)‘⟨𝑥, 𝑐⟩)
63	61, 62, 1	3eltr4g 2879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑥[,)𝑐) ∈ 𝐼)
64		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑖 ∈ 𝐼 ↔ (𝑥[,)𝑐) ∈ 𝐼))
65	63, 64	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑖 = (𝑥[,)𝑐) → 𝑖 ∈ 𝐼))
66	65	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → 𝑖 ∈ 𝐼)
67		ioof 13480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
68		ffn 6705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (,) Fn (ℝ* × ℝ*)
70		ovelrn 7588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
72		iooelexlt 38036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥)
73		df-rex 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (∃𝑦 ∈ (𝑎(,)𝑏)𝑦 < 𝑥 ↔ ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
74	72, 73	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
75		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → 𝑦 ∈ (𝑎(,)𝑏)))
77	53	elmpocl2 7655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑦 ∈ (𝑥[,)𝑐) → 𝑐 ∈ ℝ*)
78		elioore 13408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
79		elico2 13443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
80	78, 79	sylan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐)))
81		simp2 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐) → 𝑥 ≤ 𝑦)
82	80, 81	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑐 ∈ ℝ*) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
83	82	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑐 ∈ ℝ* → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦)))
84	83	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → (𝑐 ∈ ℝ* → 𝑥 ≤ 𝑦)))
85	77, 84	mpdi 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → 𝑥 ≤ 𝑦))
86	85	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ≤ 𝑦)
87	78	rexrd 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ*)
88	87	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑥 ∈ ℝ*)
89		elicore 13431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
90	78, 89	sylan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ)
91	90	rexrd 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → 𝑦 ∈ ℝ*)
92		xrlenlt 11280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥))
93	92	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 → ¬ 𝑦 < 𝑥))
94	93	con2d 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
95	88, 91, 94	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → (𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦))
96	86, 95	mt2d 137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ 𝑦 < 𝑥)
97	96	intnand 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑦 ∈ (𝑥[,)𝑐)) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥))
98	97	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑦 ∈ (𝑥[,)𝑐) → ¬ (𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥)))
99	98	con2d 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ 𝑦 ∈ (𝑥[,)𝑐)))
100	76, 99	jcad 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → (𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐))))
101		annim 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑦 ∈ (𝑎(,)𝑏) ∧ ¬ 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
102	100, 101	imbitrdi 254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
103	102	eximdv 1946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (∃𝑦(𝑦 ∈ (𝑎(,)𝑏) ∧ 𝑦 < 𝑥) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐))))
104	74, 103	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
105		exnal 1856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∃𝑦 ¬ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)) ↔ ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
106	104, 105	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
107		df-ss 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎(,)𝑏) ⊆ (𝑥[,)𝑐) ↔ ∀𝑦(𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑥[,)𝑐)))
108	106, 107	sylnibr 332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
109		imnan 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) → ¬ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)) ↔ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
110	108, 109	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ¬ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))
111		eleq2 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
112		sseq1 3961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑜 ⊆ (𝑥[,)𝑐) ↔ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐)))
113	111, 112	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑥[,)𝑐))))
114	110, 113	mtbiri 330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑜 = (𝑎(,)𝑏) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐)))
115		sseq2 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ (𝑥[,)𝑐)))
116	115	anbi2d 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = (𝑥[,)𝑐) → ((𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
117	116	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = (𝑥[,)𝑐) → (¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ (𝑥[,)𝑐))))
118	114, 117	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
120	119	rexlimivv 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
121	71, 120	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑜 ∈ ran (,) → (𝑖 = (𝑥[,)𝑐) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
122	121	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 = (𝑥[,)𝑐) → (𝑜 ∈ ran (,) → ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
123	122	ralrimiv 3155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (𝑥[,)𝑐) → ∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
124		ralnex 3090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑜 ∈ ran (,) ¬ (𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖) ↔ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
125	123, 124	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (𝑥[,)𝑐) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
126	125	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))
127	66, 126	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
128	127	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
129	49, 128	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
130		an12 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
131		annim 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
132	131	anbi2i 634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖 ∈ 𝐼 ∧ (𝑥 ∈ 𝑖 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
133	130, 132	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ 𝑖 ∧ (𝑖 ∈ 𝐼 ∧ ¬ ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) ↔ (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
134	129, 133	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → (𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
135		rspe 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ 𝐼 ∧ ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
136	134, 135	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
137		rexnal 3116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑖 ∈ 𝐼 ¬ (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
138	136, 137	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ) ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
139	138	exp41 439	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ → (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
140	139	com4l 93	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ ℝ → (𝑥 < 𝑐 → (𝑖 = (𝑥[,)𝑐) → (𝑥 ∈ ℝ → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))))
141	140	imp41 430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
142		rspe 3254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
143	34, 141, 142	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
144		rexnal 3116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ ℝ ¬ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
145	143, 144	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
146		df-ico 13384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ [,) = (𝑚 ∈ ℝ*, 𝑛 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛)})
147	146	ixxex 13389	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ [,) ∈ V
148		imaexg 7908	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([,) ∈ V → ([,) “ (ℝ × ℝ)) ∈ V)
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([,) “ (ℝ × ℝ)) ∈ V
150	1, 149	eqeltri 2858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 ∈ V
151	1	icoreunrn 38033	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ 𝐼
152		unirnioo 13482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ = ∪ ran (,)
153	151, 152	eqtr3i 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝐼 = ∪ ran (,)
154		tgss2 23155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,)) → ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖))))
155	150, 153, 154	mp2an 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
156	151	raleqi 3320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)) ↔ ∀𝑥 ∈ ∪ 𝐼∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
157	155, 156	bitr4i 281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘𝐼) ⊆ (topGen‘ran (,)) ↔ ∀𝑥 ∈ ℝ ∀𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 → ∃𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖)))
158	145, 157	sylnibr 332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
159	158	sbcth 3758	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]((((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
161		sbcimg 3791	. . . . . . . . . . . . . . . . . 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 233	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) → [1 / 𝑥] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
164		sbcel1v 3808	. . . . . . . . . . . . . . . . . 18 ⊢ ([1 / 𝑥]𝑥 ∈ ℝ ↔ 1 ∈ ℝ)
165	7, 164	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ [1 / 𝑥]𝑥 ∈ ℝ
166		sbcan 3792	. . . . . . . . . . . . . . . . 17 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ [1 / 𝑥]𝑥 ∈ ℝ))
167	165, 166	mpbiran2 722	. . . . . . . . . . . . . . . 16 ⊢ ([1 / 𝑥](((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) ∧ 𝑥 ∈ ℝ) ↔ [1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)))
168		sbcg 3815	. . . . . . . . . . . . . . . . 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 294	. . . . . . . . . . . . . . 15 ⊢ ([1 / 𝑥]((𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ 𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
171	33, 170	sylbir 238	. . . . . . . . . . . . . 14 ⊢ (([1 / 𝑥](𝑐 ∈ ℝ ∧ 𝑥 < 𝑐) ∧ [1 / 𝑥]𝑖 = (𝑥[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
172	21, 32, 171	syl2anbr 610	. . . . . . . . . . . . 13 ⊢ (((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
173	172	sbcth 3758	. . . . . . . . . . . 12 ⊢ ((1[,)𝑐) ∈ V → [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
174	5, 173	ax-mp 5	. . . . . . . . . . 11 ⊢ [(1[,)𝑐) / 𝑖](((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
175		sbcimg 3791	. . . . . . . . . . . 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 233	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) → [(1[,)𝑐) / 𝑖] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
178		sbcan 3792	. . . . . . . . . . 11 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
179		eqid 2762	. . . . . . . . . . . . 13 ⊢ (1[,)𝑐) = (1[,)𝑐)
180		eqsbc1 3789	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐)))
181	5, 180	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐) ↔ (1[,)𝑐) = (1[,)𝑐))
182	179, 181	mpbir 234	. . . . . . . . . . . 12 ⊢ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)
183		sbcg 3815	. . . . . . . . . . . . . 14 ⊢ ((1[,)𝑐) ∈ V → ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐)))
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
185	184	anbi1i 635	. . . . . . . . . . . 12 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)))
186	182, 185	mpbiran2 722	. . . . . . . . . . 11 ⊢ (([(1[,)𝑐) / 𝑖](𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ [(1[,)𝑐) / 𝑖]𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
187	178, 186	bitri 278	. . . . . . . . . 10 ⊢ ([(1[,)𝑐) / 𝑖]((𝑐 ∈ ℝ ∧ 1 < 𝑐) ∧ 𝑖 = (1[,)𝑐)) ↔ (𝑐 ∈ ℝ ∧ 1 < 𝑐))
188		sbcg 3815	. . . . . . . . . . 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 294	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
191	190	sbcth 3758	. . . . . . . 8 ⊢ (2 ∈ ℝ → [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))))
192	3, 191	ax-mp 5	. . . . . . 7 ⊢ [2 / 𝑐]((𝑐 ∈ ℝ ∧ 1 < 𝑐) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
193		sbcimg 3791	. . . . . . . 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 233	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) → [2 / 𝑐] ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
196		sbcan 3792	. . . . . . 7 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ ([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐))
197		sbcel1v 3808	. . . . . . . 8 ⊢ ([2 / 𝑐]𝑐 ∈ ℝ ↔ 2 ∈ ℝ)
198		sbcbr123 5164	. . . . . . . . 9 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ ⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐)
199		csbconstg 3871	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌1 = 1)
200	3, 199	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌1 = 1
201		csbvarg 4398	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌𝑐 = 2)
202	3, 201	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌𝑐 = 2
203	200, 202	breq12i 5117	. . . . . . . . 9 ⊢ (⦋2 / 𝑐⦌1⦋2 / 𝑐⦌ < ⦋2 / 𝑐⦌𝑐 ↔ 1⦋2 / 𝑐⦌ < 2)
204		csbconstg 3871	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → ⦋2 / 𝑐⦌ < = < )
205	3, 204	ax-mp 5	. . . . . . . . . 10 ⊢ ⦋2 / 𝑐⦌ < = <
206	205	breqi 5114	. . . . . . . . 9 ⊢ (1⦋2 / 𝑐⦌ < 2 ↔ 1 < 2)
207	198, 203, 206	3bitri 300	. . . . . . . 8 ⊢ ([2 / 𝑐]1 < 𝑐 ↔ 1 < 2)
208	197, 207	anbi12i 639	. . . . . . 7 ⊢ (([2 / 𝑐]𝑐 ∈ ℝ ∧ [2 / 𝑐]1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
209	196, 208	bitri 278	. . . . . 6 ⊢ ([2 / 𝑐](𝑐 ∈ ℝ ∧ 1 < 𝑐) ↔ (2 ∈ ℝ ∧ 1 < 2))
210		sbcg 3815	. . . . . . 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 294	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,)))
213	3, 4, 212	mp2an 704	. . . 4 ⊢ ¬ (topGen‘𝐼) ⊆ (topGen‘ran (,))
214		eqimss 3994	. . . 4 ⊢ ((topGen‘𝐼) = (topGen‘ran (,)) → (topGen‘𝐼) ⊆ (topGen‘ran (,)))
215	213, 214	mto 200	. . 3 ⊢ ¬ (topGen‘𝐼) = (topGen‘ran (,))
216	215	nesymir 3015	. 2 ⊢ (topGen‘ran (,)) ≠ (topGen‘𝐼)
217		df-pss 3924	. 2 ⊢ ((topGen‘ran (,)) ⊊ (topGen‘𝐼) ↔ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ∧ (topGen‘ran (,)) ≠ (topGen‘𝐼)))
218	2, 216, 217	mpbir2an 723	1 ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3415  Vcvv 3454  [wsbc 3743  ⦋csb 3852   ⊆ wss 3904   ⊊ wpss 3905  𝒫 cpw 4561  ⟨cop 4594  ∪ cuni 4871   class class class wbr 5108   × cxp 5658  dom cdm 5660  ran crn 5661   “ cima 5663  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7412  ℝcr 11105  1c1 11107  ℝ^*cxr 11248   < clt 11249   ≤ cle 11250  2c2 12301  (,)cioo 13378  [,)cico 13380  topGenctg 17496

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-ioo 13382  df-ico 13384  df-topgen 17502

This theorem is used by: (None)