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

Theorem mnfnei 22316
Description: A neighborhood of -∞ contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
mnfnei ((𝐴 ∈ (ordTop‘ ≤ ) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem mnfnei
Dummy variables 𝑎 𝑏 𝑐 𝑢 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . . 4 ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
2 eqid 2737 . . . 4 ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
3 eqid 2737 . . . 4 ran (,) = ran (,)
41, 2, 3leordtval 22308 . . 3 (ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)))
54eleq2i 2828 . 2 (𝐴 ∈ (ordTop‘ ≤ ) ↔ 𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,))))
6 tg2 22059 . . 3 ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ -∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,))(-∞ ∈ 𝑢𝑢𝐴))
7 elun 4084 . . . . 5 (𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)))
8 elun 4084 . . . . . . 7 (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ↔ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))))
9 eqid 2737 . . . . . . . . . . 11 (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
109elrnmpt 5859 . . . . . . . . . 10 (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ* 𝑢 = (𝑦(,]+∞)))
1110elv 3433 . . . . . . . . 9 (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔ ∃𝑦 ∈ ℝ* 𝑢 = (𝑦(,]+∞))
12 nltmnf 12810 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → ¬ 𝑦 < -∞)
13 pnfxr 10976 . . . . . . . . . . . . . . . 16 +∞ ∈ ℝ*
14 elioc1 13066 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (-∞ ∈ (𝑦(,]+∞) ↔ (-∞ ∈ ℝ*𝑦 < -∞ ∧ -∞ ≤ +∞)))
1513, 14mpan2 687 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ* → (-∞ ∈ (𝑦(,]+∞) ↔ (-∞ ∈ ℝ*𝑦 < -∞ ∧ -∞ ≤ +∞)))
16 simp2 1135 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 < -∞ ∧ -∞ ≤ +∞) → 𝑦 < -∞)
1715, 16syl6bi 252 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → (-∞ ∈ (𝑦(,]+∞) → 𝑦 < -∞))
1812, 17mtod 197 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ¬ -∞ ∈ (𝑦(,]+∞))
19 eleq2 2825 . . . . . . . . . . . . . 14 (𝑢 = (𝑦(,]+∞) → (-∞ ∈ 𝑢 ↔ -∞ ∈ (𝑦(,]+∞)))
2019notbid 317 . . . . . . . . . . . . 13 (𝑢 = (𝑦(,]+∞) → (¬ -∞ ∈ 𝑢 ↔ ¬ -∞ ∈ (𝑦(,]+∞)))
2118, 20syl5ibrcom 246 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (𝑢 = (𝑦(,]+∞) → ¬ -∞ ∈ 𝑢))
2221rexlimiv 3207 . . . . . . . . . . 11 (∃𝑦 ∈ ℝ* 𝑢 = (𝑦(,]+∞) → ¬ -∞ ∈ 𝑢)
2322pm2.21d 121 . . . . . . . . . 10 (∃𝑦 ∈ ℝ* 𝑢 = (𝑦(,]+∞) → (-∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
2423adantrd 491 . . . . . . . . 9 (∃𝑦 ∈ ℝ* 𝑢 = (𝑦(,]+∞) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
2511, 24sylbi 216 . . . . . . . 8 (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
26 eqid 2737 . . . . . . . . . . 11 (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
2726elrnmpt 5859 . . . . . . . . . 10 (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ* 𝑢 = (-∞[,)𝑦)))
2827elv 3433 . . . . . . . . 9 (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ↔ ∃𝑦 ∈ ℝ* 𝑢 = (-∞[,)𝑦))
29 mnfxr 10979 . . . . . . . . . . . . . 14 -∞ ∈ ℝ*
3029a1i 11 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → -∞ ∈ ℝ*)
31 0xr 10969 . . . . . . . . . . . . . 14 0 ∈ ℝ*
32 simprl 767 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → 𝑦 ∈ ℝ*)
33 ifcl 4506 . . . . . . . . . . . . . 14 ((0 ∈ ℝ*𝑦 ∈ ℝ*) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*)
3431, 32, 33sylancr 586 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*)
3513a1i 11 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → +∞ ∈ ℝ*)
36 mnflt0 12806 . . . . . . . . . . . . . 14 -∞ < 0
37 simpll 763 . . . . . . . . . . . . . . . . 17 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → -∞ ∈ 𝑢)
38 simprr 769 . . . . . . . . . . . . . . . . 17 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → 𝑢 = (-∞[,)𝑦))
3937, 38eleqtrd 2839 . . . . . . . . . . . . . . . 16 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → -∞ ∈ (-∞[,)𝑦))
40 elico1 13067 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*) → (-∞ ∈ (-∞[,)𝑦) ↔ (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦)))
4129, 32, 40sylancr 586 . . . . . . . . . . . . . . . 16 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → (-∞ ∈ (-∞[,)𝑦) ↔ (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦)))
4239, 41mpbid 231 . . . . . . . . . . . . . . 15 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦))
4342simp3d 1142 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → -∞ < 𝑦)
44 breq2 5079 . . . . . . . . . . . . . . 15 (0 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞ < 0 ↔ -∞ < if(0 ≤ 𝑦, 0, 𝑦)))
45 breq2 5079 . . . . . . . . . . . . . . 15 (𝑦 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞ < 𝑦 ↔ -∞ < if(0 ≤ 𝑦, 0, 𝑦)))
4644, 45ifboth 4500 . . . . . . . . . . . . . 14 ((-∞ < 0 ∧ -∞ < 𝑦) → -∞ < if(0 ≤ 𝑦, 0, 𝑦))
4736, 43, 46sylancr 586 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → -∞ < if(0 ≤ 𝑦, 0, 𝑦))
4831a1i 11 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → 0 ∈ ℝ*)
49 xrmin1 12856 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ*𝑦 ∈ ℝ*) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 0)
5031, 32, 49sylancr 586 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 0)
51 0re 10924 . . . . . . . . . . . . . . 15 0 ∈ ℝ
52 ltpnf 12801 . . . . . . . . . . . . . . 15 (0 ∈ ℝ → 0 < +∞)
5351, 52mp1i 13 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → 0 < +∞)
5434, 48, 35, 50, 53xrlelttrd 12839 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) < +∞)
55 xrre2 12849 . . . . . . . . . . . . 13 (((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) < +∞)) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ)
5630, 34, 35, 47, 54, 55syl32anc 1376 . . . . . . . . . . . 12 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ)
57 xrmin2 12857 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ*𝑦 ∈ ℝ*) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦)
5831, 32, 57sylancr 586 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦)
59 df-ico 13030 . . . . . . . . . . . . . . 15 [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎𝑐𝑐 < 𝑏)})
60 xrltletr 12836 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*𝑦 ∈ ℝ*) → ((𝑥 < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → 𝑥 < 𝑦))
6159, 59, 60ixxss2 13043 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦))
6232, 58, 61syl2anc 583 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦))
63 simplr 765 . . . . . . . . . . . . . 14 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → 𝑢𝐴)
6438, 63eqsstrrd 3961 . . . . . . . . . . . . 13 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → (-∞[,)𝑦) ⊆ 𝐴)
6562, 64sstrd 3932 . . . . . . . . . . . 12 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴)
66 oveq2 7268 . . . . . . . . . . . . . 14 (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞[,)𝑥) = (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)))
6766sseq1d 3953 . . . . . . . . . . . . 13 (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → ((-∞[,)𝑥) ⊆ 𝐴 ↔ (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴))
6867rspcev 3557 . . . . . . . . . . . 12 ((if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ ∧ (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
6956, 65, 68syl2anc 583 . . . . . . . . . . 11 (((-∞ ∈ 𝑢𝑢𝐴) ∧ (𝑦 ∈ ℝ*𝑢 = (-∞[,)𝑦))) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
7069rexlimdvaa 3212 . . . . . . . . . 10 ((-∞ ∈ 𝑢𝑢𝐴) → (∃𝑦 ∈ ℝ* 𝑢 = (-∞[,)𝑦) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
7170com12 32 . . . . . . . . 9 (∃𝑦 ∈ ℝ* 𝑢 = (-∞[,)𝑦) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
7228, 71sylbi 216 . . . . . . . 8 (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
7325, 72jaoi 853 . . . . . . 7 ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
748, 73sylbi 216 . . . . . 6 (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
75 mnfnre 10965 . . . . . . . . . 10 -∞ ∉ ℝ
7675neli 3049 . . . . . . . . 9 ¬ -∞ ∈ ℝ
77 elssuni 4873 . . . . . . . . . . 11 (𝑢 ∈ ran (,) → 𝑢 ran (,))
78 unirnioo 13126 . . . . . . . . . . 11 ℝ = ran (,)
7977, 78sseqtrrdi 3973 . . . . . . . . . 10 (𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ)
8079sseld 3921 . . . . . . . . 9 (𝑢 ∈ ran (,) → (-∞ ∈ 𝑢 → -∞ ∈ ℝ))
8176, 80mtoi 198 . . . . . . . 8 (𝑢 ∈ ran (,) → ¬ -∞ ∈ 𝑢)
8281pm2.21d 121 . . . . . . 7 (𝑢 ∈ ran (,) → (-∞ ∈ 𝑢 → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
8382adantrd 491 . . . . . 6 (𝑢 ∈ ran (,) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
8474, 83jaoi 853 . . . . 5 ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∨ 𝑢 ∈ ran (,)) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
857, 84sylbi 216 . . . 4 (𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴))
8685rexlimiv 3207 . . 3 (∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,))(-∞ ∈ 𝑢𝑢𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
876, 86syl 17 . 2 ((𝐴 ∈ (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,))) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
885, 87sylanb 580 1 ((𝐴 ∈ (ordTop‘ ≤ ) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843  w3a 1085   = wceq 1539  wcel 2107  wrex 3063  Vcvv 3427  cun 3886  wss 3888  ifcif 4461   cuni 4841   class class class wbr 5075  cmpt 5158  ran crn 5586  cfv 6423  (class class class)co 7260  cr 10817  0cc0 10818  +∞cpnf 10953  -∞cmnf 10954  *cxr 10955   < clt 10956  cle 10957  (,)cioo 13024  (,]cioc 13025  [,)cico 13026  topGenctg 17092  ordTopcordt 17154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4842  df-int 4882  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-ord 6259  df-on 6260  df-lim 6261  df-suc 6262  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-om 7693  df-1st 7809  df-2nd 7810  df-1o 8272  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-fin 8700  df-fi 9116  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-ioo 13028  df-ioc 13029  df-ico 13030  df-icc 13031  df-topgen 17098  df-ordt 17156  df-ps 18228  df-tsr 18229  df-top 21987  df-bases 22040
This theorem is referenced by:  xlimmnfvlem2  43306
  Copyright terms: Public domain W3C validator