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

Theorem lecldbas 21862
 Description: The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypothesis
Ref Expression
lecldbas.1 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ*𝑥))
Assertion
Ref Expression
lecldbas (ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹))

Proof of Theorem lecldbas
Dummy variables 𝑎 𝑏 𝑐 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2798 . . . 4 ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
2 eqid 2798 . . . 4 ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
31, 2leordtval2 21855 . . 3 (ordTop‘ ≤ ) = (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))))
4 fvex 6665 . . . 4 (fi‘ran 𝐹) ∈ V
5 fvex 6665 . . . . . 6 (ordTop‘ ≤ ) ∈ V
6 lecldbas.1 . . . . . . . 8 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ*𝑥))
7 iccf 12843 . . . . . . . . . . 11 [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
8 ffn 6492 . . . . . . . . . . 11 ([,]:(ℝ* × ℝ*)⟶𝒫 ℝ* → [,] Fn (ℝ* × ℝ*))
97, 8ax-mp 5 . . . . . . . . . 10 [,] Fn (ℝ* × ℝ*)
10 ovelrn 7312 . . . . . . . . . 10 ([,] Fn (ℝ* × ℝ*) → (𝑥 ∈ ran [,] ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏)))
119, 10ax-mp 5 . . . . . . . . 9 (𝑥 ∈ ran [,] ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏))
12 difeq2 4046 . . . . . . . . . . . 12 (𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) = (ℝ* ∖ (𝑎[,]𝑏)))
13 iccordt 21857 . . . . . . . . . . . . 13 (𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤ ))
14 letopuni 21850 . . . . . . . . . . . . . 14 * = (ordTop‘ ≤ )
1514cldopn 21674 . . . . . . . . . . . . 13 ((𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤ )) → (ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤ ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤ )
1712, 16eqeltrdi 2898 . . . . . . . . . . 11 (𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
1817rexlimivw 3241 . . . . . . . . . 10 (∃𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
1918rexlimivw 3241 . . . . . . . . 9 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
2011, 19sylbi 220 . . . . . . . 8 (𝑥 ∈ ran [,] → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
216, 20fmpti 6860 . . . . . . 7 𝐹:ran [,]⟶(ordTop‘ ≤ )
22 frn 6498 . . . . . . 7 (𝐹:ran [,]⟶(ordTop‘ ≤ ) → ran 𝐹 ⊆ (ordTop‘ ≤ ))
2321, 22ax-mp 5 . . . . . 6 ran 𝐹 ⊆ (ordTop‘ ≤ )
245, 23ssexi 5193 . . . . 5 ran 𝐹 ∈ V
25 eqid 2798 . . . . . . . 8 (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
26 mnfxr 10702 . . . . . . . . . . 11 -∞ ∈ ℝ*
27 fnovrn 7311 . . . . . . . . . . 11 (([,] Fn (ℝ* × ℝ*) ∧ -∞ ∈ ℝ*𝑦 ∈ ℝ*) → (-∞[,]𝑦) ∈ ran [,])
289, 26, 27mp3an12 1448 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (-∞[,]𝑦) ∈ ran [,])
2926a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → -∞ ∈ ℝ*)
30 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ*𝑦 ∈ ℝ*)
31 pnfxr 10699 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
3231a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → +∞ ∈ ℝ*)
33 mnfle 12534 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → -∞ ≤ 𝑦)
34 pnfge 12530 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ*𝑦 ≤ +∞)
35 df-icc 12750 . . . . . . . . . . . . . . 15 [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎𝑐𝑐𝑏)})
36 df-ioc 12748 . . . . . . . . . . . . . . 15 (,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐𝑐𝑏)})
37 xrltnle 10712 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (𝑦 < 𝑧 ↔ ¬ 𝑧𝑦))
38 xrletr 12556 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧𝑦𝑦 ≤ +∞) → 𝑧 ≤ +∞))
39 xrlelttr 12554 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦 < 𝑧) → -∞ < 𝑧))
40 xrltle 12547 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ*𝑧 ∈ ℝ*) → (-∞ < 𝑧 → -∞ ≤ 𝑧))
41403adant2 1128 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (-∞ < 𝑧 → -∞ ≤ 𝑧))
4239, 41syld 47 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦 < 𝑧) → -∞ ≤ 𝑧))
4335, 36, 37, 35, 38, 42ixxun 12759 . . . . . . . . . . . . . 14 (((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≤ 𝑦𝑦 ≤ +∞)) → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = (-∞[,]+∞))
4429, 30, 32, 33, 34, 43syl32anc 1375 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = (-∞[,]+∞))
45 iccmax 12818 . . . . . . . . . . . . 13 (-∞[,]+∞) = ℝ*
4644, 45eqtrdi 2849 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ*)
47 iccssxr 12825 . . . . . . . . . . . . 13 (-∞[,]𝑦) ⊆ ℝ*
4835, 36, 37ixxdisj 12758 . . . . . . . . . . . . . 14 ((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅)
4926, 31, 48mp3an13 1449 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅)
50 uneqdifeq 4398 . . . . . . . . . . . . 13 (((-∞[,]𝑦) ⊆ ℝ* ∧ ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅) → (((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞)))
5147, 49, 50sylancr 590 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞)))
5246, 51mpbid 235 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞))
5352eqcomd 2804 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (𝑦(,]+∞) = (ℝ* ∖ (-∞[,]𝑦)))
54 difeq2 4046 . . . . . . . . . . 11 (𝑥 = (-∞[,]𝑦) → (ℝ*𝑥) = (ℝ* ∖ (-∞[,]𝑦)))
5554rspceeqv 3586 . . . . . . . . . 10 (((-∞[,]𝑦) ∈ ran [,] ∧ (𝑦(,]+∞) = (ℝ* ∖ (-∞[,]𝑦))) → ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
5628, 53, 55syl2anc 587 . . . . . . . . 9 (𝑦 ∈ ℝ* → ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
57 xrex 12391 . . . . . . . . . . 11 * ∈ V
5857difexi 5199 . . . . . . . . . 10 (ℝ*𝑥) ∈ V
596, 58elrnmpti 5799 . . . . . . . . 9 ((𝑦(,]+∞) ∈ ran 𝐹 ↔ ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
6056, 59sylibr 237 . . . . . . . 8 (𝑦 ∈ ℝ* → (𝑦(,]+∞) ∈ ran 𝐹)
6125, 60fmpti 6860 . . . . . . 7 (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)):ℝ*⟶ran 𝐹
62 frn 6498 . . . . . . 7 ((𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)):ℝ*⟶ran 𝐹 → ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ⊆ ran 𝐹)
6361, 62ax-mp 5 . . . . . 6 ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ⊆ ran 𝐹
64 eqid 2798 . . . . . . . 8 (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
65 fnovrn 7311 . . . . . . . . . . 11 (([,] Fn (ℝ* × ℝ*) ∧ 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑦[,]+∞) ∈ ran [,])
669, 31, 65mp3an13 1449 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (𝑦[,]+∞) ∈ ran [,])
67 df-ico 12749 . . . . . . . . . . . . . . 15 [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎𝑐𝑐 < 𝑏)})
68 xrlenlt 10710 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (𝑦𝑧 ↔ ¬ 𝑧 < 𝑦))
69 xrltletr 12555 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦𝑦 ≤ +∞) → 𝑧 < +∞))
70 xrltle 12547 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤ +∞))
71703adant2 1128 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤ +∞))
7269, 71syld 47 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦𝑦 ≤ +∞) → 𝑧 ≤ +∞))
73 xrletr 12556 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦𝑧) → -∞ ≤ 𝑧))
7467, 35, 68, 35, 72, 73ixxun 12759 . . . . . . . . . . . . . 14 (((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≤ 𝑦𝑦 ≤ +∞)) → ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = (-∞[,]+∞))
7529, 30, 32, 33, 34, 74syl32anc 1375 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = (-∞[,]+∞))
76 uncom 4082 . . . . . . . . . . . . 13 ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = ((𝑦[,]+∞) ∪ (-∞[,)𝑦))
7775, 76, 453eqtr3g 2856 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → ((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ*)
78 iccssxr 12825 . . . . . . . . . . . . 13 (𝑦[,]+∞) ⊆ ℝ*
79 incom 4130 . . . . . . . . . . . . . 14 ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ((-∞[,)𝑦) ∩ (𝑦[,]+∞))
8067, 35, 68ixxdisj 12758 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞[,)𝑦) ∩ (𝑦[,]+∞)) = ∅)
8126, 31, 80mp3an13 1449 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → ((-∞[,)𝑦) ∩ (𝑦[,]+∞)) = ∅)
8279, 81syl5eq 2845 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ∅)
83 uneqdifeq 4398 . . . . . . . . . . . . 13 (((𝑦[,]+∞) ⊆ ℝ* ∧ ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ∅) → (((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦)))
8478, 82, 83sylancr 590 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦)))
8577, 84mpbid 235 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦))
8685eqcomd 2804 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (-∞[,)𝑦) = (ℝ* ∖ (𝑦[,]+∞)))
87 difeq2 4046 . . . . . . . . . . 11 (𝑥 = (𝑦[,]+∞) → (ℝ*𝑥) = (ℝ* ∖ (𝑦[,]+∞)))
8887rspceeqv 3586 . . . . . . . . . 10 (((𝑦[,]+∞) ∈ ran [,] ∧ (-∞[,)𝑦) = (ℝ* ∖ (𝑦[,]+∞))) → ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
8966, 86, 88syl2anc 587 . . . . . . . . 9 (𝑦 ∈ ℝ* → ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
906, 58elrnmpti 5799 . . . . . . . . 9 ((-∞[,)𝑦) ∈ ran 𝐹 ↔ ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
9189, 90sylibr 237 . . . . . . . 8 (𝑦 ∈ ℝ* → (-∞[,)𝑦) ∈ ran 𝐹)
9264, 91fmpti 6860 . . . . . . 7 (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹
93 frn 6498 . . . . . . 7 ((𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹 → ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ⊆ ran 𝐹)
9492, 93ax-mp 5 . . . . . 6 ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ⊆ ran 𝐹
9563, 94unssi 4114 . . . . 5 (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ⊆ ran 𝐹
96 fiss 8887 . . . . 5 ((ran 𝐹 ∈ V ∧ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ⊆ ran 𝐹) → (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹))
9724, 95, 96mp2an 691 . . . 4 (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹)
98 tgss 21611 . . . 4 (((fi‘ran 𝐹) ∈ V ∧ (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹)) → (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))))) ⊆ (topGen‘(fi‘ran 𝐹)))
994, 97, 98mp2an 691 . . 3 (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))))) ⊆ (topGen‘(fi‘ran 𝐹))
1003, 99eqsstri 3950 . 2 (ordTop‘ ≤ ) ⊆ (topGen‘(fi‘ran 𝐹))
101 letop 21849 . . 3 (ordTop‘ ≤ ) ∈ Top
102 tgfiss 21634 . . 3 (((ordTop‘ ≤ ) ∈ Top ∧ ran 𝐹 ⊆ (ordTop‘ ≤ )) → (topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤ ))
103101, 23, 102mp2an 691 . 2 (topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤ )
104100, 103eqssi 3932 1 (ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441   ∖ cdif 3879   ∪ cun 3880   ∩ cin 3881   ⊆ wss 3882  ∅c0 4245  𝒫 cpw 4499   class class class wbr 5033   ↦ cmpt 5113   × cxp 5520  ran crn 5523   Fn wfn 6324  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142  ficfi 8873  +∞cpnf 10676  -∞cmnf 10677  ℝ*cxr 10678   < clt 10679   ≤ cle 10680  (,]cioc 12744  [,)cico 12745  [,]cicc 12746  topGenctg 16720  ordTopcordt 16781  Topctop 21536  Clsdccld 21659 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fi 8874  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-ioc 12748  df-ico 12749  df-icc 12750  df-topgen 16726  df-ordt 16783  df-ps 17819  df-tsr 17820  df-top 21537  df-topon 21554  df-bases 21589  df-cld 21662 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator