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 23162

Description: A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 24749 (which describes neighborhoods of ℝ) and mnfnei 23163, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23159 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 2734	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
2		eqid 2734	. . . 4 ⊢ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
3		eqid 2734	. . . 4 ⊢ ran (,) = ran (,)
4	1, 2, 3	leordtval 23155	. . 3 ⊢ (ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)))
5	4	eleq2i 2826	. 2 ⊢ (𝐴 ∈ (ordTop‘ ≤ ) ↔ 𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))))
6		tg2 22907	. . 3 ⊢ ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ +∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴))
7		elun 4103	. . . . 5 ⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)))
8		elun 4103	. . . . . . 7 ⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ↔ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))))
9		eqid 2734	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞))
10	9	elrnmpt 5905	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞)))
11	10	elv 3443	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞))
12		mnfxr 11187	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
13	12	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ ∈ ℝ^*)
14		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ∈ ℝ^*)
15		0xr 11177	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
16		ifcl 4523	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ^* ∧ 0 ∈ ℝ^) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^)
17	14, 15, 16	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^*)
18		pnfxr 11184	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ ℝ^*)
20		xrmax1 13088	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
21	15, 14, 20	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
22		ge0gtmnf 13085	. . . . . . . . . . . . . 14 ⊢ ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) → -∞ < if(0 ≤ 𝑦, 𝑦, 0))
23	17, 21, 22	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ < if(0 ≤ 𝑦, 𝑦, 0))
24		simpll 766	. . . . . . . . . . . . . . . . 17 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ 𝑢)
25		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 = (𝑦(,]+∞))
26	24, 25	eleqtrd 2836	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ (𝑦(,]+∞))
27		elioc1 13301	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^ ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
28	14, 18, 27	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞)))
29	26, 28	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ ℝ^* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞))
30	29	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 < +∞)
31		0ltpnf 13034	. . . . . . . . . . . . . 14 ⊢ 0 < +∞
32		breq1 5099	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑦 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
33		breq1 5099	. . . . . . . . . . . . . . 15 ⊢ (0 = if(0 ≤ 𝑦, 𝑦, 0) → (0 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞))
34	32, 33	ifboth 4517	. . . . . . . . . . . . . 14 ⊢ ((𝑦 < +∞ ∧ 0 < +∞) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
35	30, 31, 34	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) < +∞)
36		xrre2 13083	. . . . . . . . . . . . 13 ⊢ (((-∞ ∈ ℝ^* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ < if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
37	13, 17, 19, 23, 35, 36	syl32anc 1380	. . . . . . . . . . . 12 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
38		xrmax2 13089	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
39	15, 14, 38	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
40		df-ioc 13264	. . . . . . . . . . . . . . 15 ⊢ (,] = (𝑎 ∈ ℝ^, 𝑏 ∈ ℝ^ ↦ {𝑐 ∈ ℝ^* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)})
41		xrlelttr 13068	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ^* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → ((𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < 𝑥) → 𝑦 < 𝑥))
42	40, 40, 41	ixxss1 13277	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞))
43	14, 39, 42	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞))
44		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 ⊆ 𝐴)
45	25, 44	eqsstrrd 3967	. . . . . . . . . . . . 13 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (𝑦(,]+∞) ⊆ 𝐴)
46	43, 45	sstrd 3942	. . . . . . . . . . . 12 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴)
47		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑥(,]+∞) = (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞))
48	47	sseq1d 3963	. . . . . . . . . . . . 13 ⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴))
49	48	rspcev 3574	. . . . . . . . . . . 12 ⊢ ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
50	37, 46, 49	syl2anc 584	. . . . . . . . . . 11 ⊢ (((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ^* ∧ 𝑢 = (𝑦(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
51	50	rexlimdvaa 3136	. . . . . . . . . 10 ⊢ ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
52	51	com12 32	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (𝑦(,]+∞) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
53	11, 52	sylbi 217	. . . . . . . 8 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
54		eqid 2734	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))
55	54	elrnmpt 5905	. . . . . . . . . 10 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦)))
56	55	elv 3443	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦))
57		pnfnlt 13040	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ^* → ¬ +∞ < 𝑦)
58		elico1 13302	. . . . . . . . . . . . . . . 16 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ^ ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦)))
59	12, 58	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ^* → (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ^* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦)))
60		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((+∞ ∈ ℝ^* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦) → +∞ < 𝑦)
61	59, 60	biimtrdi 253	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ^* → (+∞ ∈ (-∞[,)𝑦) → +∞ < 𝑦))
62	57, 61	mtod 198	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ^* → ¬ +∞ ∈ (-∞[,)𝑦))
63		eleq2 2823	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 ↔ +∞ ∈ (-∞[,)𝑦)))
64	63	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑢 = (-∞[,)𝑦) → (¬ +∞ ∈ 𝑢 ↔ ¬ +∞ ∈ (-∞[,)𝑦)))
65	62, 64	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ^* → (𝑢 = (-∞[,)𝑦) → ¬ +∞ ∈ 𝑢))
66	65	rexlimiv 3128	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → ¬ +∞ ∈ 𝑢)
67	66	pm2.21d 121	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
68	67	adantrd 491	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ℝ^* 𝑢 = (-∞[,)𝑦) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
69	56, 68	sylbi 217	. . . . . . . 8 ⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
70	53, 69	jaoi 857	. . . . . . 7 ⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
71	8, 70	sylbi 217	. . . . . 6 ⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
72		pnfnre 11171	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
73	72	neli 3036	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
74		elssuni 4892	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,))
75		unirnioo 13363	. . . . . . . . . . 11 ⊢ ℝ = ∪ ran (,)
76	74, 75	sseqtrrdi 3973	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ)
77	76	sseld 3930	. . . . . . . . 9 ⊢ (𝑢 ∈ ran (,) → (+∞ ∈ 𝑢 → +∞ ∈ ℝ))
78	73, 77	mtoi 199	. . . . . . . 8 ⊢ (𝑢 ∈ ran (,) → ¬ +∞ ∈ 𝑢)
79	78	pm2.21d 121	. . . . . . 7 ⊢ (𝑢 ∈ ran (,) → (+∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
80	79	adantrd 491	. . . . . 6 ⊢ (𝑢 ∈ ran (,) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
81	71, 80	jaoi 857	. . . . 5 ⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
82	7, 81	sylbi 217	. . . 4 ⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴))
83	82	rexlimiv 3128	. . 3 ⊢ (∃𝑢 ∈ ((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
84	6, 83	syl 17	. 2 ⊢ ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ^* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ^* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
85	5, 84	sylanb 581	1 ⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∃wrex 3058 Vcvv 3438 ∪ cun 3897 ⊆ wss 3899 ifcif 4477 ∪ cuni 4861 class class class wbr 5096 ↦ cmpt 5177 ran crn 5623 ‘cfv 6490 (class class class)co 7356 ℝcr 11023 0cc0 11024 +∞cpnf 11161 -∞cmnf 11162 ℝ^*cxr 11163 < clt 11164 ≤ cle 11165 (,)cioo 13259 (,]cioc 13260 [,)cico 13261 topGenctg 17355 ordTopcordt 17418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-1o 8395 df-2o 8396 df-er 8633 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-fi 9312 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-ioo 13263 df-ioc 13264 df-ico 13265 df-icc 13266 df-topgen 17361 df-ordt 17420 df-ps 18487 df-tsr 18488 df-top 22836 df-bases 22888

This theorem is referenced by: xrge0tsms 24777 xrlimcnp 26932 xrge0tsmsd 33104 pnfneige0 34057 xlimpnfvlem2 46023

W3C validator