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

Theorem opnreen 24853
Description: Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.)
Assertion
Ref Expression
opnreen ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ)

Proof of Theorem opnreen
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 11246 . . . 4 ℝ ∈ V
2 elssuni 4937 . . . . 5 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 (topGen‘ran (,)))
3 uniretop 24783 . . . . 5 ℝ = (topGen‘ran (,))
42, 3sseqtrrdi 4025 . . . 4 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ℝ)
5 ssdomg 9040 . . . 4 (ℝ ∈ V → (𝐴 ⊆ ℝ → 𝐴 ≼ ℝ))
61, 4, 5mpsyl 68 . . 3 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ≼ ℝ)
7 rpnnen 16263 . . 3 ℝ ≈ 𝒫 ℕ
8 domentr 9053 . . 3 ((𝐴 ≼ ℝ ∧ ℝ ≈ 𝒫 ℕ) → 𝐴 ≼ 𝒫 ℕ)
96, 7, 8sylancl 586 . 2 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ≼ 𝒫 ℕ)
10 n0 4353 . . . 4 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
114sselda 3983 . . . . . . . . 9 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
12 rpnnen2 16262 . . . . . . . . . . . 12 𝒫 ℕ ≼ (0[,]1)
13 rphalfcl 13062 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
1413rpred 13077 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
15 resubcl 11573 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ) → (𝑥 − (𝑦 / 2)) ∈ ℝ)
1614, 15sylan2 593 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 − (𝑦 / 2)) ∈ ℝ)
17 readdcl 11238 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ) → (𝑥 + (𝑦 / 2)) ∈ ℝ)
1814, 17sylan2 593 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + (𝑦 / 2)) ∈ ℝ)
19 simpl 482 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝑥 ∈ ℝ)
20 ltsubrp 13071 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ+) → (𝑥 − (𝑦 / 2)) < 𝑥)
2113, 20sylan2 593 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 − (𝑦 / 2)) < 𝑥)
22 ltaddrp 13072 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ+) → 𝑥 < (𝑥 + (𝑦 / 2)))
2313, 22sylan2 593 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝑥 < (𝑥 + (𝑦 / 2)))
2416, 19, 18, 21, 23lttrd 11422 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 − (𝑦 / 2)) < (𝑥 + (𝑦 / 2)))
25 iccen 13537 . . . . . . . . . . . . 13 (((𝑥 − (𝑦 / 2)) ∈ ℝ ∧ (𝑥 + (𝑦 / 2)) ∈ ℝ ∧ (𝑥 − (𝑦 / 2)) < (𝑥 + (𝑦 / 2))) → (0[,]1) ≈ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))))
2616, 18, 24, 25syl3anc 1373 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (0[,]1) ≈ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))))
27 domentr 9053 . . . . . . . . . . . 12 ((𝒫 ℕ ≼ (0[,]1) ∧ (0[,]1) ≈ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2)))) → 𝒫 ℕ ≼ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))))
2812, 26, 27sylancr 587 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝒫 ℕ ≼ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))))
29 ovex 7464 . . . . . . . . . . . 12 ((𝑥𝑦)(,)(𝑥 + 𝑦)) ∈ V
30 rpre 13043 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
31 resubcl 11573 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦) ∈ ℝ)
3230, 31sylan2 593 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥𝑦) ∈ ℝ)
3332rexrd 11311 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥𝑦) ∈ ℝ*)
34 readdcl 11238 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
3530, 34sylan2 593 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + 𝑦) ∈ ℝ)
3635rexrd 11311 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + 𝑦) ∈ ℝ*)
3719recnd 11289 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝑥 ∈ ℂ)
3814adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
3938recnd 11289 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℂ)
4037, 39, 39subsub4d 11651 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 − (𝑦 / 2)) − (𝑦 / 2)) = (𝑥 − ((𝑦 / 2) + (𝑦 / 2))))
4130adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
4241recnd 11289 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
43422halvesd 12512 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
4443oveq2d 7447 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 − ((𝑦 / 2) + (𝑦 / 2))) = (𝑥𝑦))
4540, 44eqtrd 2777 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 − (𝑦 / 2)) − (𝑦 / 2)) = (𝑥𝑦))
4613adantl 481 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ+)
4716, 46ltsubrpd 13109 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 − (𝑦 / 2)) − (𝑦 / 2)) < (𝑥 − (𝑦 / 2)))
4845, 47eqbrtrrd 5167 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥𝑦) < (𝑥 − (𝑦 / 2)))
4918, 46ltaddrpd 13110 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + (𝑦 / 2)) < ((𝑥 + (𝑦 / 2)) + (𝑦 / 2)))
5037, 39, 39addassd 11283 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 + (𝑦 / 2)) + (𝑦 / 2)) = (𝑥 + ((𝑦 / 2) + (𝑦 / 2))))
5143oveq2d 7447 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + ((𝑦 / 2) + (𝑦 / 2))) = (𝑥 + 𝑦))
5250, 51eqtrd 2777 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 + (𝑦 / 2)) + (𝑦 / 2)) = (𝑥 + 𝑦))
5349, 52breqtrd 5169 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥 + (𝑦 / 2)) < (𝑥 + 𝑦))
54 iccssioo 13456 . . . . . . . . . . . . 13 ((((𝑥𝑦) ∈ ℝ* ∧ (𝑥 + 𝑦) ∈ ℝ*) ∧ ((𝑥𝑦) < (𝑥 − (𝑦 / 2)) ∧ (𝑥 + (𝑦 / 2)) < (𝑥 + 𝑦))) → ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ⊆ ((𝑥𝑦)(,)(𝑥 + 𝑦)))
5533, 36, 48, 53, 54syl22anc 839 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ⊆ ((𝑥𝑦)(,)(𝑥 + 𝑦)))
56 ssdomg 9040 . . . . . . . . . . . 12 (((𝑥𝑦)(,)(𝑥 + 𝑦)) ∈ V → (((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ⊆ ((𝑥𝑦)(,)(𝑥 + 𝑦)) → ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ≼ ((𝑥𝑦)(,)(𝑥 + 𝑦))))
5729, 55, 56mpsyl 68 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ≼ ((𝑥𝑦)(,)(𝑥 + 𝑦)))
58 domtr 9047 . . . . . . . . . . 11 ((𝒫 ℕ ≼ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ∧ ((𝑥 − (𝑦 / 2))[,](𝑥 + (𝑦 / 2))) ≼ ((𝑥𝑦)(,)(𝑥 + 𝑦))) → 𝒫 ℕ ≼ ((𝑥𝑦)(,)(𝑥 + 𝑦)))
5928, 57, 58syl2anc 584 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝒫 ℕ ≼ ((𝑥𝑦)(,)(𝑥 + 𝑦)))
60 eqid 2737 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
6160bl2ioo 24813 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) = ((𝑥𝑦)(,)(𝑥 + 𝑦)))
6230, 61sylan2 593 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) = ((𝑥𝑦)(,)(𝑥 + 𝑦)))
6359, 62breqtrrd 5171 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → 𝒫 ℕ ≼ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦))
6411, 63sylan 580 . . . . . . . 8 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) ∧ 𝑦 ∈ ℝ+) → 𝒫 ℕ ≼ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦))
65 simplll 775 . . . . . . . . 9 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴) → 𝐴 ∈ (topGen‘ran (,)))
66 simpr 484 . . . . . . . . 9 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴) → (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴)
67 ssdomg 9040 . . . . . . . . 9 (𝐴 ∈ (topGen‘ran (,)) → ((𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴 → (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ≼ 𝐴))
6865, 66, 67sylc 65 . . . . . . . 8 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴) → (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ≼ 𝐴)
69 domtr 9047 . . . . . . . 8 ((𝒫 ℕ ≼ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ∧ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ≼ 𝐴) → 𝒫 ℕ ≼ 𝐴)
7064, 68, 69syl2an2r 685 . . . . . . 7 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴) → 𝒫 ℕ ≼ 𝐴)
71 eqid 2737 . . . . . . . . . 10 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7260, 71tgioo 24817 . . . . . . . . 9 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7372eleq2i 2833 . . . . . . . 8 (𝐴 ∈ (topGen‘ran (,)) ↔ 𝐴 ∈ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))))
7460rexmet 24812 . . . . . . . . 9 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
7571mopni2 24506 . . . . . . . . 9 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐴 ∈ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) ∧ 𝑥𝐴) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴)
7674, 75mp3an1 1450 . . . . . . . 8 ((𝐴 ∈ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) ∧ 𝑥𝐴) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴)
7773, 76sylanb 581 . . . . . . 7 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑦) ⊆ 𝐴)
7870, 77r19.29a 3162 . . . . . 6 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑥𝐴) → 𝒫 ℕ ≼ 𝐴)
7978ex 412 . . . . 5 (𝐴 ∈ (topGen‘ran (,)) → (𝑥𝐴 → 𝒫 ℕ ≼ 𝐴))
8079exlimdv 1933 . . . 4 (𝐴 ∈ (topGen‘ran (,)) → (∃𝑥 𝑥𝐴 → 𝒫 ℕ ≼ 𝐴))
8110, 80biimtrid 242 . . 3 (𝐴 ∈ (topGen‘ran (,)) → (𝐴 ≠ ∅ → 𝒫 ℕ ≼ 𝐴))
8281imp 406 . 2 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝒫 ℕ ≼ 𝐴)
83 sbth 9133 . 2 ((𝐴 ≼ 𝒫 ℕ ∧ 𝒫 ℕ ≼ 𝐴) → 𝐴 ≈ 𝒫 ℕ)
849, 82, 83syl2an2r 685 1 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wex 1779  wcel 2108  wne 2940  wrex 3070  Vcvv 3480  wss 3951  c0 4333  𝒫 cpw 4600   cuni 4907   class class class wbr 5143   × cxp 5683  ran crn 5686  cres 5687  ccom 5689  cfv 6561  (class class class)co 7431  cen 8982  cdom 8983  cr 11154  0cc0 11155  1c1 11156   + caddc 11158  *cxr 11294   < clt 11295  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  +crp 13034  (,)cioo 13387  [,]cicc 13390  abscabs 15273  topGenctg 17482  ∞Metcxmet 21349  ballcbl 21351  MetOpencmopn 21354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-omul 8511  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-acn 9982  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953
This theorem is referenced by:  rectbntr0  24854
  Copyright terms: Public domain W3C validator