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

Theorem lecldbas 22116
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 2737 . . . 4 ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
2 eqid 2737 . . . 4 ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
31, 2leordtval2 22109 . . 3 (ordTop‘ ≤ ) = (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))))
4 fvex 6730 . . . 4 (fi‘ran 𝐹) ∈ V
5 fvex 6730 . . . . . 6 (ordTop‘ ≤ ) ∈ V
6 lecldbas.1 . . . . . . . 8 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ*𝑥))
7 iccf 13036 . . . . . . . . . . 11 [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
8 ffn 6545 . . . . . . . . . . 11 ([,]:(ℝ* × ℝ*)⟶𝒫 ℝ* → [,] Fn (ℝ* × ℝ*))
97, 8ax-mp 5 . . . . . . . . . 10 [,] Fn (ℝ* × ℝ*)
10 ovelrn 7384 . . . . . . . . . 10 ([,] Fn (ℝ* × ℝ*) → (𝑥 ∈ ran [,] ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏)))
119, 10ax-mp 5 . . . . . . . . 9 (𝑥 ∈ ran [,] ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏))
12 difeq2 4031 . . . . . . . . . . . 12 (𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) = (ℝ* ∖ (𝑎[,]𝑏)))
13 iccordt 22111 . . . . . . . . . . . . 13 (𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤ ))
14 letopuni 22104 . . . . . . . . . . . . . 14 * = (ordTop‘ ≤ )
1514cldopn 21928 . . . . . . . . . . . . 13 ((𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤ )) → (ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤ ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤ )
1712, 16eqeltrdi 2846 . . . . . . . . . . 11 (𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
1817rexlimivw 3201 . . . . . . . . . 10 (∃𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
1918rexlimivw 3201 . . . . . . . . 9 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏) → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
2011, 19sylbi 220 . . . . . . . 8 (𝑥 ∈ ran [,] → (ℝ*𝑥) ∈ (ordTop‘ ≤ ))
216, 20fmpti 6929 . . . . . . 7 𝐹:ran [,]⟶(ordTop‘ ≤ )
22 frn 6552 . . . . . . 7 (𝐹:ran [,]⟶(ordTop‘ ≤ ) → ran 𝐹 ⊆ (ordTop‘ ≤ ))
2321, 22ax-mp 5 . . . . . 6 ran 𝐹 ⊆ (ordTop‘ ≤ )
245, 23ssexi 5215 . . . . 5 ran 𝐹 ∈ V
25 eqid 2737 . . . . . . . 8 (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) = (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞))
26 mnfxr 10890 . . . . . . . . . . 11 -∞ ∈ ℝ*
27 fnovrn 7383 . . . . . . . . . . 11 (([,] Fn (ℝ* × ℝ*) ∧ -∞ ∈ ℝ*𝑦 ∈ ℝ*) → (-∞[,]𝑦) ∈ ran [,])
289, 26, 27mp3an12 1453 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (-∞[,]𝑦) ∈ ran [,])
2926a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → -∞ ∈ ℝ*)
30 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ*𝑦 ∈ ℝ*)
31 pnfxr 10887 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
3231a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → +∞ ∈ ℝ*)
33 mnfle 12726 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → -∞ ≤ 𝑦)
34 pnfge 12722 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ*𝑦 ≤ +∞)
35 df-icc 12942 . . . . . . . . . . . . . . 15 [,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎𝑐𝑐𝑏)})
36 df-ioc 12940 . . . . . . . . . . . . . . 15 (,] = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐𝑐𝑏)})
37 xrltnle 10900 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (𝑦 < 𝑧 ↔ ¬ 𝑧𝑦))
38 xrletr 12748 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧𝑦𝑦 ≤ +∞) → 𝑧 ≤ +∞))
39 xrlelttr 12746 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦 < 𝑧) → -∞ < 𝑧))
40 xrltle 12739 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ*𝑧 ∈ ℝ*) → (-∞ < 𝑧 → -∞ ≤ 𝑧))
41403adant2 1133 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (-∞ < 𝑧 → -∞ ≤ 𝑧))
4239, 41syld 47 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦 < 𝑧) → -∞ ≤ 𝑧))
4335, 36, 37, 35, 38, 42ixxun 12951 . . . . . . . . . . . . . 14 (((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≤ 𝑦𝑦 ≤ +∞)) → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = (-∞[,]+∞))
4429, 30, 32, 33, 34, 43syl32anc 1380 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = (-∞[,]+∞))
45 iccmax 13011 . . . . . . . . . . . . 13 (-∞[,]+∞) = ℝ*
4644, 45eqtrdi 2794 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ*)
47 iccssxr 13018 . . . . . . . . . . . . 13 (-∞[,]𝑦) ⊆ ℝ*
4835, 36, 37ixxdisj 12950 . . . . . . . . . . . . . 14 ((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅)
4926, 31, 48mp3an13 1454 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅)
50 uneqdifeq 4404 . . . . . . . . . . . . 13 (((-∞[,]𝑦) ⊆ ℝ* ∧ ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅) → (((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞)))
5147, 49, 50sylancr 590 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (((-∞[,]𝑦) ∪ (𝑦(,]+∞)) = ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞)))
5246, 51mpbid 235 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞))
5352eqcomd 2743 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (𝑦(,]+∞) = (ℝ* ∖ (-∞[,]𝑦)))
54 difeq2 4031 . . . . . . . . . . 11 (𝑥 = (-∞[,]𝑦) → (ℝ*𝑥) = (ℝ* ∖ (-∞[,]𝑦)))
5554rspceeqv 3552 . . . . . . . . . 10 (((-∞[,]𝑦) ∈ ran [,] ∧ (𝑦(,]+∞) = (ℝ* ∖ (-∞[,]𝑦))) → ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
5628, 53, 55syl2anc 587 . . . . . . . . 9 (𝑦 ∈ ℝ* → ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
57 xrex 12583 . . . . . . . . . . 11 * ∈ V
5857difexi 5221 . . . . . . . . . 10 (ℝ*𝑥) ∈ V
596, 58elrnmpti 5829 . . . . . . . . 9 ((𝑦(,]+∞) ∈ ran 𝐹 ↔ ∃𝑥 ∈ ran [,](𝑦(,]+∞) = (ℝ*𝑥))
6056, 59sylibr 237 . . . . . . . 8 (𝑦 ∈ ℝ* → (𝑦(,]+∞) ∈ ran 𝐹)
6125, 60fmpti 6929 . . . . . . 7 (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)):ℝ*⟶ran 𝐹
62 frn 6552 . . . . . . 7 ((𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)):ℝ*⟶ran 𝐹 → ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ⊆ ran 𝐹)
6361, 62ax-mp 5 . . . . . 6 ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ⊆ ran 𝐹
64 eqid 2737 . . . . . . . 8 (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) = (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))
65 fnovrn 7383 . . . . . . . . . . 11 (([,] Fn (ℝ* × ℝ*) ∧ 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑦[,]+∞) ∈ ran [,])
669, 31, 65mp3an13 1454 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (𝑦[,]+∞) ∈ ran [,])
67 df-ico 12941 . . . . . . . . . . . . . . 15 [,) = (𝑎 ∈ ℝ*, 𝑏 ∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎𝑐𝑐 < 𝑏)})
68 xrlenlt 10898 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → (𝑦𝑧 ↔ ¬ 𝑧 < 𝑦))
69 xrltletr 12747 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦𝑦 ≤ +∞) → 𝑧 < +∞))
70 xrltle 12739 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤ +∞))
71703adant2 1133 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤ +∞))
7269, 71syld 47 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦𝑦 ≤ +∞) → 𝑧 ≤ +∞))
73 xrletr 12748 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((-∞ ≤ 𝑦𝑦𝑧) → -∞ ≤ 𝑧))
7467, 35, 68, 35, 72, 73ixxun 12951 . . . . . . . . . . . . . 14 (((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≤ 𝑦𝑦 ≤ +∞)) → ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = (-∞[,]+∞))
7529, 30, 32, 33, 34, 74syl32anc 1380 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = (-∞[,]+∞))
76 uncom 4067 . . . . . . . . . . . . 13 ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) = ((𝑦[,]+∞) ∪ (-∞[,)𝑦))
7775, 76, 453eqtr3g 2801 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → ((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ*)
78 iccssxr 13018 . . . . . . . . . . . . 13 (𝑦[,]+∞) ⊆ ℝ*
79 incom 4115 . . . . . . . . . . . . . 14 ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ((-∞[,)𝑦) ∩ (𝑦[,]+∞))
8067, 35, 68ixxdisj 12950 . . . . . . . . . . . . . . 15 ((-∞ ∈ ℝ*𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞[,)𝑦) ∩ (𝑦[,]+∞)) = ∅)
8126, 31, 80mp3an13 1454 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → ((-∞[,)𝑦) ∩ (𝑦[,]+∞)) = ∅)
8279, 81syl5eq 2790 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ∅)
83 uneqdifeq 4404 . . . . . . . . . . . . 13 (((𝑦[,]+∞) ⊆ ℝ* ∧ ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ∅) → (((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦)))
8478, 82, 83sylancr 590 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (((𝑦[,]+∞) ∪ (-∞[,)𝑦)) = ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦)))
8577, 84mpbid 235 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦))
8685eqcomd 2743 . . . . . . . . . 10 (𝑦 ∈ ℝ* → (-∞[,)𝑦) = (ℝ* ∖ (𝑦[,]+∞)))
87 difeq2 4031 . . . . . . . . . . 11 (𝑥 = (𝑦[,]+∞) → (ℝ*𝑥) = (ℝ* ∖ (𝑦[,]+∞)))
8887rspceeqv 3552 . . . . . . . . . 10 (((𝑦[,]+∞) ∈ ran [,] ∧ (-∞[,)𝑦) = (ℝ* ∖ (𝑦[,]+∞))) → ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
8966, 86, 88syl2anc 587 . . . . . . . . 9 (𝑦 ∈ ℝ* → ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
906, 58elrnmpti 5829 . . . . . . . . 9 ((-∞[,)𝑦) ∈ ran 𝐹 ↔ ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ*𝑥))
9189, 90sylibr 237 . . . . . . . 8 (𝑦 ∈ ℝ* → (-∞[,)𝑦) ∈ ran 𝐹)
9264, 91fmpti 6929 . . . . . . 7 (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹
93 frn 6552 . . . . . . 7 ((𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹 → ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ⊆ ran 𝐹)
9492, 93ax-mp 5 . . . . . 6 ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)) ⊆ ran 𝐹
9563, 94unssi 4099 . . . . 5 (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ⊆ ran 𝐹
96 fiss 9040 . . . . 5 ((ran 𝐹 ∈ V ∧ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))) ⊆ ran 𝐹) → (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹))
9724, 95, 96mp2an 692 . . . 4 (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹)
98 tgss 21865 . . . 4 (((fi‘ran 𝐹) ∈ V ∧ (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦)))) ⊆ (fi‘ran 𝐹)) → (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))))) ⊆ (topGen‘(fi‘ran 𝐹)))
994, 97, 98mp2an 692 . . 3 (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦ (-∞[,)𝑦))))) ⊆ (topGen‘(fi‘ran 𝐹))
1003, 99eqsstri 3935 . 2 (ordTop‘ ≤ ) ⊆ (topGen‘(fi‘ran 𝐹))
101 letop 22103 . . 3 (ordTop‘ ≤ ) ∈ Top
102 tgfiss 21888 . . 3 (((ordTop‘ ≤ ) ∈ Top ∧ ran 𝐹 ⊆ (ordTop‘ ≤ )) → (topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤ ))
103101, 23, 102mp2an 692 . 2 (topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤ )
104100, 103eqssi 3917 1 (ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wrex 3062  Vcvv 3408  cdif 3863  cun 3864  cin 3865  wss 3866  c0 4237  𝒫 cpw 4513   class class class wbr 5053  cmpt 5135   × cxp 5549  ran crn 5552   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  ficfi 9026  +∞cpnf 10864  -∞cmnf 10865  *cxr 10866   < clt 10867  cle 10868  (,]cioc 12936  [,)cico 12937  [,]cicc 12938  topGenctg 16942  ordTopcordt 17004  Topctop 21790  Clsdccld 21913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fi 9027  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-ioc 12940  df-ico 12941  df-icc 12942  df-topgen 16948  df-ordt 17006  df-ps 18072  df-tsr 18073  df-top 21791  df-topon 21808  df-bases 21843  df-cld 21916
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator