Theorem iocpnfordt 21512

Description: An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)

Assertion

Ref	Expression
iocpnfordt	⊢ (𝐴(,]+∞) ∈ (ordTop‘ ≤ )

Proof of Theorem iocpnfordt

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2795	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))
2		eqid 2795	. . . . . . . . 9 ⊢ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))
3		eqid 2795	. . . . . . . . 9 ⊢ ran (,) = ran (,)
4	1, 2, 3	leordtval 21510	. . . . . . . 8 ⊢ (ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)))
5		letop 21503	. . . . . . . 8 ⊢ (ordTop‘ ≤ ) ∈ Top
6	4, 5	eqeltrri 2880	. . . . . . 7 ⊢ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))) ∈ Top
7		tgclb 21267	. . . . . . 7 ⊢ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))) ∈ Top)
8	6, 7	mpbir 232	. . . . . 6 ⊢ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ∈ TopBases
9		bastg 21263	. . . . . 6 ⊢ (((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ∈ TopBases → ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ⊆ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))))
10	8, 9	ax-mp 5	. . . . 5 ⊢ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ⊆ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)))
11	10, 4	sseqtr4i 3929	. . . 4 ⊢ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)) ⊆ (ordTop‘ ≤ )
12		ssun1 4073	. . . . 5 ⊢ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ⊆ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,))
13		ssun1 4073	. . . . . 6 ⊢ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ⊆ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)))
14		eqid 2795	. . . . . . . 8 ⊢ (𝐴(,]+∞) = (𝐴(,]+∞)
15		oveq1 7028	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥(,]+∞) = (𝐴(,]+∞))
16	15	rspceeqv 3577	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐴(,]+∞) = (𝐴(,]+∞)) → ∃𝑥 ∈ ℝ* (𝐴(,]+∞) = (𝑥(,]+∞))
17	14, 16	mpan2 687	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ∃𝑥 ∈ ℝ* (𝐴(,]+∞) = (𝑥(,]+∞))
18		eqid 2795	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) = (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))
19		ovex 7053	. . . . . . . 8 ⊢ (𝑥(,]+∞) ∈ V
20	18, 19	elrnmpti 5719	. . . . . . 7 ⊢ ((𝐴(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔ ∃𝑥 ∈ ℝ* (𝐴(,]+∞) = (𝑥(,]+∞))
21	17, 20	sylibr 235	. . . . . 6 ⊢ (𝐴 ∈ ℝ* → (𝐴(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)))
22	13, 21	sseldi 3891	. . . . 5 ⊢ (𝐴 ∈ ℝ* → (𝐴(,]+∞) ∈ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))))
23	12, 22	sseldi 3891	. . . 4 ⊢ (𝐴 ∈ ℝ* → (𝐴(,]+∞) ∈ ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))) ∪ ran (,)))
24	11, 23	sseldi 3891	. . 3 ⊢ (𝐴 ∈ ℝ* → (𝐴(,]+∞) ∈ (ordTop‘ ≤ ))
25	24	adantr 481	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) ∈ (ordTop‘ ≤ ))
26		df-ioc 12598	. . . . . 6 ⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
27	26	ixxf 12603	. . . . 5 ⊢ (,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
28	27	fdmi 6397	. . . 4 ⊢ dom (,] = (ℝ* × ℝ*)
29	28	ndmov 7193	. . 3 ⊢ (¬ (𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) = ∅)
30		0opn 21201	. . . 4 ⊢ ((ordTop‘ ≤ ) ∈ Top → ∅ ∈ (ordTop‘ ≤ ))
31	5, 30	ax-mp 5	. . 3 ⊢ ∅ ∈ (ordTop‘ ≤ )
32	29, 31	syl6eqel 2891	. 2 ⊢ (¬ (𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) ∈ (ordTop‘ ≤ ))
33	25, 32	pm2.61i 183	1 ⊢ (𝐴(,]+∞) ∈ (ordTop‘ ≤ )

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∃wrex 3106   ∪ cun 3861   ⊆ wss 3863  ∅c0 4215  𝒫 cpw 4457   ↦ cmpt 5045   × cxp 5446  ran crn 5449  ‘cfv 6230  (class class class)co 7021  +∞cpnf 10523  -∞cmnf 10524  ℝ^*cxr 10525   < clt 10526   ≤ cle 10527  (,)cioo 12593  (,]cioc 12594  [,)cico 12595  topGenctg 16545  ordTopcordt 16606  Topctop 21190  TopBasesctb 21242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-1o 7958  df-oadd 7962  df-er 8144  df-en 8363  df-dom 8364  df-sdom 8365  df-fin 8366  df-fi 8726  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-ioo 12597  df-ioc 12598  df-ico 12599  df-icc 12600  df-topgen 16551  df-ordt 16608  df-ps 17644  df-tsr 17645  df-top 21191  df-topon 21208  df-bases 21243

This theorem is referenced by:  xrlimcnp  25233  pnfneige0  30816  lmxrge0  30817  xlimpnfvlem1  41684