pnfnei - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pnfnei		Structured version Visualization version GIF version

Theorem pnfnei 23547

Description: A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 25135 (which describes neighborhoods of ℝ) and mnfnei 23548, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23544 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.)

**Assertion**
Ref	Expression
pnfnei	⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)

Distinct variable group: 𝑥,𝐴

Proof of Theorem pnfnei Dummy variables 𝑎 𝑏 𝑐 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2760	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
2		eqid 2760	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
3		eqid 2760	. . . 4 ⊢ ran (,) = ran (,)
4	1, 2, 3	leordtval 23540	. . 3 ⊢ (ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)))
5	4	eleq2i 2852	. 2 ⊢ (𝐴 ∈ (ordTop‘ ≤ ) ↔ 𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))))
6		tg2 23292	. . 3 ⊢ ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ +∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴))
7		elun 4151	. . . . 5 ⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)))
8		elun 4151	. . . . . . 7 ⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ↔ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))))
9		eqid 2760	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
10	9	elrnmpt 5941	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞)))
11	10	elv 3455	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞))
12		mnfxr 11373	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
13	12	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ ∈ ℝ^*)
14		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ∈ ℝ^*)
15		0xr 11363	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
16		ifcl 4527	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ^* ∧ 0 ∈ ℝ^) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^)
17	14, 15, 16	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^*)
18		pnfxr 11370	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ ℝ^*)
20		xrmax1 13312	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
21	15, 14, 20	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
22		ge0gtmnf 13309	. . . . . . . . . . . . . 14 ⊢ ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) → -∞ < if(0 ≤ 𝑦, 𝑦, 0))
23	17, 21, 22	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ < if(0 ≤ 𝑦, 𝑦, 0))
24		simpll 779	. . . . . . . . . . . . . . . . 17 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ 𝑢)
25		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 = (𝑦(,]+∞))
26	24, 25	eleqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ (𝑦(,]+∞))
27		elioc1 13525	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^ ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
28	14, 18, 27	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
29	26, 28	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞))
30	29	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 < +∞)
31		0ltpnf 13258	. . . . . . . . . . . . . 14 ⊢ 0 < +∞
32		breq1 5105	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑦 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
33		breq1 5105	. . . . . . . . . . . . . . 15 ⊢ (0 = if(0 ≤ 𝑦, 𝑦, 0) → (0 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
34	32, 33	ifboth 4521	. . . . . . . . . . . . . 14 ⊢ ((𝑦 < +∞ ∧ 0 < +∞) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
35	30, 31, 34	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
36		xrre2 13307	. . . . . . . . . . . . 13 ⊢ (((-∞ ∈ ℝ^* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ < if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
37	13, 17, 19, 23, 35, 36	syl32anc 1405	. . . . . . . . . . . 12 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
38		xrmax2 13313	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
39	15, 14, 38	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
40		df-ioc 13488	. . . . . . . . . . . . . . 15 ⊢ (,] = (𝑎 ∈ ℝ^, 𝑏 ∈ ℝ^ ↦ {𝑐 ∈ ℝ^* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)})
41		xrlelttr 13292	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ^* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → ((𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < 𝑥) → 𝑦 < 𝑥))
42	40, 40, 41	ixxss1 13501	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞))
43	14, 39, 42	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞))
44		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 ⊆ 𝐴)
45	25, 44	eqsstrrd 3944	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (𝑦(,]+∞) ⊆ 𝐴)
46	43, 45	sstrd 3919	. . . . . . . . . . . 12 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴)
47		oveq1 7431	. . . . . . . . . . . . . 14 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑥(,]+∞) = (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞))
48	47	sseq1d 3940	. . . . . . . . . . . . 13 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴))
49	48	rspcev 3576	. . . . . . . . . . . 12 ⊢ ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
50	37, 46, 49	syl2anc 596	. . . . . . . . . . 11 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
51	50	rexlimdvaa 3164	. . . . . . . . . 10 ⊢ ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
52	51	com12 33	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
53	11, 52	sylbi 220	. . . . . . . 8 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
54		eqid 2760	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
55	54	elrnmpt 5941	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦)))
56	55	elv 3455	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦))
57		pnfnlt 13264	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ^* → ¬ +∞ < 𝑦)
58		elico1 13526	. . . . . . . . . . . . . . . 16 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ^ ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦)))
59	12, 58	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ^* → (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ^* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦)))
60		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ ((+∞ ∈ ℝ^* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦) → +∞ < 𝑦)
61	59, 60	biimtrdi 256	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ^* → (+∞ ∈ (-∞[,)𝑦) → +∞ < 𝑦))
62	57, 61	mtod 201	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ^* → ¬ +∞ ∈ (-∞[,)𝑦))
63		eleq2 2849	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 ↔ +∞ ∈ (-∞[,)𝑦)))
64	63	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑢 = (-∞[,)𝑦) → (¬ +∞ ∈ 𝑢 ↔ ¬ +∞ ∈ (-∞[,)𝑦)))
65	62, 64	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ^* → (𝑢 = (-∞[,)𝑦) → ¬ +∞ ∈ 𝑢))
66	65	rexlimiv 3156	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → ¬ +∞ ∈ 𝑢)
67	66	pm2.21d 122	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
68	67	adantrd 497	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
69	56, 68	sylbi 220	. . . . . . . 8 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
70	53, 69	jaoi 871	. . . . . . 7 ⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
71	8, 70	sylbi 220	. . . . . 6 ⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
72		pnfnre 11357	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
73	72	neli 3063	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
74		elssuni 4898	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,))
75		unirnioo 13587	. . . . . . . . . . 11 ⊢ ℝ = ∪ ran (,)
76	74, 75	sseqtrrdi 3950	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ)
77	76	sseld 3908	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (,) → (+∞ ∈ 𝑢 → +∞ ∈ ℝ))
78	73, 77	mtoi 202	. . . . . . . 8 ⊢ (𝑢 ∈ ran (,) → ¬ +∞ ∈ 𝑢)
79	78	pm2.21d 122	. . . . . . 7 ⊢ (𝑢 ∈ ran (,) → (+∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
80	79	adantrd 497	. . . . . 6 ⊢ (𝑢 ∈ ran (,) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
81	71, 80	jaoi 871	. . . . 5 ⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
82	7, 81	sylbi 220	. . . 4 ⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
83	82	rexlimiv 3156	. . 3 ⊢ (∃𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
84	6, 83	syl 18	. 2 ⊢ ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
85	5, 84	sylanb 593	1 ⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 Vcvv 3450 ⊆ wss 3896 ∪ cun 4148 ifcif 4481 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 ran crn 5652 ‘cfv 6543 (class class class)co 7424 ℝcr 11206 0cc0 11207 +∞cpnf 11347 -∞cmnf 11348 ℝ^*cxr 11349 < clt 11350 ≤ cle 11351 (,)cioo 13483 (,]cioc 13484 [,)cico 13485 topGenctg 17617 ordTopcordt 17680

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-1o 8483 df-2o 8484 df-er 8724 df-en 8981 df-dom 8982 df-sdom 8983 df-fin 8984 df-fi 9410 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-ioo 13487 df-ioc 13488 df-ico 13489 df-icc 13490 df-topgen 17623 df-ordt 17682 df-ps 18749 df-tsr 18750 df-top 23221 df-bases 23273

This theorem is used by: xrge0tsms 25163 xrlimcnp 27305 xrge0tsmsd 33684 pnfneige0 34633 xlimpnfvlem2 46955

W3C validator