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 23531

Description: A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 25119 (which describes neighborhoods of ℝ) and mnfnei 23532, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23528 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 2761	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
2		eqid 2761	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
3		eqid 2761	. . . 4 ⊢ ran (,) = ran (,)
4	1, 2, 3	leordtval 23524	. . 3 ⊢ (ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)))
5	4	eleq2i 2853	. 2 ⊢ (𝐴 ∈ (ordTop‘ ≤ ) ↔ 𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))))
6		tg2 23276	. . 3 ⊢ ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ +∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴))
7		elun 4100	. . . . 5 ⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)))
8		elun 4100	. . . . . . 7 ⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ↔ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))))
9		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
10	9	elrnmpt 5940	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞)))
11	10	elv 3456	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞))
12		mnfxr 11359	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
13	12	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ ∈ ℝ^*)
14		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ∈ ℝ^*)
15		0xr 11349	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
16		ifcl 4528	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ^* ∧ 0 ∈ ℝ^) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^)
17	14, 15, 16	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^*)
18		pnfxr 11356	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ ℝ^*)
20		xrmax1 13298	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
21	15, 14, 20	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
22		ge0gtmnf 13295	. . . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ (𝑦(,]+∞))
27		elioc1 13511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^ ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
28	14, 18, 27	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
29	26, 28	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞))
30	29	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 < +∞)
31		0ltpnf 13244	. . . . . . . . . . . . . 14 ⊢ 0 < +∞
32		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑦 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
33		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (0 = if(0 ≤ 𝑦, 𝑦, 0) → (0 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
34	32, 33	ifboth 4522	. . . . . . . . . . . . . 14 ⊢ ((𝑦 < +∞ ∧ 0 < +∞) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
35	30, 31, 34	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
36		xrre2 13293	. . . . . . . . . . . . 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 13299	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
39	15, 14, 38	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
40		df-ioc 13474	. . . . . . . . . . . . . . 15 ⊢ (,] = (𝑎 ∈ ℝ^, 𝑏 ∈ ℝ^ ↦ {𝑐 ∈ ℝ^* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)})
41		xrlelttr 13278	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ^* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → ((𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < 𝑥) → 𝑦 < 𝑥))
42	40, 40, 41	ixxss1 13487	. . . . . . . . . . . . . 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 3966	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (𝑦(,]+∞) ⊆ 𝐴)
46	43, 45	sstrd 3941	. . . . . . . . . . . 12 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴)
47		oveq1 7425	. . . . . . . . . . . . . 14 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑥(,]+∞) = (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞))
48	47	sseq1d 3962	. . . . . . . . . . . . 13 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴))
49	48	rspcev 3577	. . . . . . . . . . . 12 ⊢ ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
50	37, 46, 49	syl2anc 596	. . . . . . . . . . 11 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
51	50	rexlimdvaa 3165	. . . . . . . . . 10 ⊢ ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
52	51	com12 33	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
53	11, 52	sylbi 220	. . . . . . . 8 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
54		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
55	54	elrnmpt 5940	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦)))
56	55	elv 3456	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦))
57		pnfnlt 13250	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ^* → ¬ +∞ < 𝑦)
58		elico1 13512	. . . . . . . . . . . . . . . 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 2850	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 ↔ +∞ ∈ (-∞[,)𝑦)))
64	63	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑢 = (-∞[,)𝑦) → (¬ +∞ ∈ 𝑢 ↔ ¬ +∞ ∈ (-∞[,)𝑦)))
65	62, 64	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ^* → (𝑢 = (-∞[,)𝑦) → ¬ +∞ ∈ 𝑢))
66	65	rexlimiv 3157	. . . . . . . . . . 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 11343	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
73	72	neli 3064	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
74		elssuni 4899	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,))
75		unirnioo 13573	. . . . . . . . . . 11 ⊢ ℝ = ∪ ran (,)
76	74, 75	sseqtrrdi 3972	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ)
77	76	sseld 3930	. . . . . . . . 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 3157	. . 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 1570 ∈ wcel 2145 ∃wrex 3087 Vcvv 3451 ∪ cun 3897 ⊆ wss 3899 ifcif 4482 ∪ cuni 4867 class class class wbr 5103 ↦ cmpt 5186 ran crn 5652 ‘cfv 6537 (class class class)co 7418 ℝcr 11192 0cc0 11193 +∞cpnf 11333 -∞cmnf 11334 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 (,)cioo 13469 (,]cioc 13470 [,)cico 13471 topGenctg 17601 ordTopcordt 17664

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 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 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-1o 8469 df-2o 8470 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fi 9396 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-topgen 17607 df-ordt 17666 df-ps 18733 df-tsr 18734 df-top 23205 df-bases 23257

This theorem is used by: xrge0tsms 25147 xrlimcnp 27289 xrge0tsmsd 33627 pnfneige0 34576 xlimpnfvlem2 46816

W3C validator