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

Theorem caublcls 23951
 Description: The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
Hypotheses
Ref Expression
caubl.2 (𝜑𝐷 ∈ (∞Met‘𝑋))
caubl.3 (𝜑𝐹:ℕ⟶(𝑋 × ℝ+))
caubl.4 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑛)))
caublcls.6 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
caublcls ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝑃 ∈ ((cls‘𝐽)‘((ball‘𝐷)‘(𝐹𝐴))))
Distinct variable groups:   𝐷,𝑛   𝑛,𝐹   𝑛,𝑋
Allowed substitution hints:   𝜑(𝑛)   𝐴(𝑛)   𝑃(𝑛)   𝐽(𝑛)

Proof of Theorem caublcls
Dummy variables 𝑘 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2798 . 2 (ℤ𝐴) = (ℤ𝐴)
2 caubl.2 . . . 4 (𝜑𝐷 ∈ (∞Met‘𝑋))
323ad2ant1 1130 . . 3 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋))
4 caublcls.6 . . . 4 𝐽 = (MetOpen‘𝐷)
54mopntopon 23084 . . 3 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
63, 5syl 17 . 2 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝐽 ∈ (TopOn‘𝑋))
7 simp3 1135 . . 3 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝐴 ∈ ℕ)
87nnzd 12091 . 2 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝐴 ∈ ℤ)
9 simp2 1134 . 2 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (1st𝐹)(⇝𝑡𝐽)𝑃)
10 2fveq3 6657 . . . . . . . 8 (𝑟 = 𝐴 → ((ball‘𝐷)‘(𝐹𝑟)) = ((ball‘𝐷)‘(𝐹𝐴)))
1110sseq1d 3947 . . . . . . 7 (𝑟 = 𝐴 → (((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) ↔ ((ball‘𝐷)‘(𝐹𝐴)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
1211imbi2d 344 . . . . . 6 (𝑟 = 𝐴 → (((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))) ↔ ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝐴)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))))
13 2fveq3 6657 . . . . . . . 8 (𝑟 = 𝑘 → ((ball‘𝐷)‘(𝐹𝑟)) = ((ball‘𝐷)‘(𝐹𝑘)))
1413sseq1d 3947 . . . . . . 7 (𝑟 = 𝑘 → (((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) ↔ ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
1514imbi2d 344 . . . . . 6 (𝑟 = 𝑘 → (((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))) ↔ ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))))
16 2fveq3 6657 . . . . . . . 8 (𝑟 = (𝑘 + 1) → ((ball‘𝐷)‘(𝐹𝑟)) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))))
1716sseq1d 3947 . . . . . . 7 (𝑟 = (𝑘 + 1) → (((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
1817imbi2d 344 . . . . . 6 (𝑟 = (𝑘 + 1) → (((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑟)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))) ↔ ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))))
19 ssid 3938 . . . . . . 7 ((ball‘𝐷)‘(𝐹𝐴)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))
20192a1i 12 . . . . . 6 (𝐴 ∈ ℤ → ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝐴)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
21 caubl.4 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑛)))
22 eluznn 12323 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝐴)) → 𝑘 ∈ ℕ)
23 fvoveq1 7165 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
2423fveq2d 6656 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))))
25 2fveq3 6657 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹𝑛)) = ((ball‘𝐷)‘(𝐹𝑘)))
2624, 25sseq12d 3949 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑘))))
2726rspccva 3570 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑛)) ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑘)))
2821, 22, 27syl2an 598 . . . . . . . . . 10 ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝐴))) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑘)))
2928anassrs 471 . . . . . . . . 9 (((𝜑𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑘)))
30 sstr2 3923 . . . . . . . . 9 (((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝑘)) → (((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
3129, 30syl 17 . . . . . . . 8 (((𝜑𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
3231expcom 417 . . . . . . 7 (𝑘 ∈ (ℤ𝐴) → ((𝜑𝐴 ∈ ℕ) → (((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))))
3332a2d 29 . . . . . 6 (𝑘 ∈ (ℤ𝐴) → (((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))) → ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))))
3412, 15, 18, 15, 20, 33uzind4 12311 . . . . 5 (𝑘 ∈ (ℤ𝐴) → ((𝜑𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴))))
3534impcom 411 . . . 4 (((𝜑𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))
36353adantl2 1164 . . 3 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((ball‘𝐷)‘(𝐹𝑘)) ⊆ ((ball‘𝐷)‘(𝐹𝐴)))
373adantr 484 . . . . 5 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
38 simpl1 1188 . . . . . . . 8 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → 𝜑)
39 caubl.3 . . . . . . . 8 (𝜑𝐹:ℕ⟶(𝑋 × ℝ+))
4038, 39syl 17 . . . . . . 7 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → 𝐹:ℕ⟶(𝑋 × ℝ+))
41223ad2antl3 1184 . . . . . . 7 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → 𝑘 ∈ ℕ)
4240, 41ffvelrnd 6836 . . . . . 6 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (𝐹𝑘) ∈ (𝑋 × ℝ+))
43 xp1st 7713 . . . . . 6 ((𝐹𝑘) ∈ (𝑋 × ℝ+) → (1st ‘(𝐹𝑘)) ∈ 𝑋)
4442, 43syl 17 . . . . 5 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (1st ‘(𝐹𝑘)) ∈ 𝑋)
45 xp2nd 7714 . . . . . 6 ((𝐹𝑘) ∈ (𝑋 × ℝ+) → (2nd ‘(𝐹𝑘)) ∈ ℝ+)
4642, 45syl 17 . . . . 5 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (2nd ‘(𝐹𝑘)) ∈ ℝ+)
47 blcntr 23058 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝐹𝑘)) ∈ 𝑋 ∧ (2nd ‘(𝐹𝑘)) ∈ ℝ+) → (1st ‘(𝐹𝑘)) ∈ ((1st ‘(𝐹𝑘))(ball‘𝐷)(2nd ‘(𝐹𝑘))))
4837, 44, 46, 47syl3anc 1368 . . . 4 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (1st ‘(𝐹𝑘)) ∈ ((1st ‘(𝐹𝑘))(ball‘𝐷)(2nd ‘(𝐹𝑘))))
49 fvco3 6744 . . . . 5 ((𝐹:ℕ⟶(𝑋 × ℝ+) ∧ 𝑘 ∈ ℕ) → ((1st𝐹)‘𝑘) = (1st ‘(𝐹𝑘)))
5040, 41, 49syl2anc 587 . . . 4 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((1st𝐹)‘𝑘) = (1st ‘(𝐹𝑘)))
51 1st2nd2 7720 . . . . . . 7 ((𝐹𝑘) ∈ (𝑋 × ℝ+) → (𝐹𝑘) = ⟨(1st ‘(𝐹𝑘)), (2nd ‘(𝐹𝑘))⟩)
5242, 51syl 17 . . . . . 6 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → (𝐹𝑘) = ⟨(1st ‘(𝐹𝑘)), (2nd ‘(𝐹𝑘))⟩)
5352fveq2d 6656 . . . . 5 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((ball‘𝐷)‘(𝐹𝑘)) = ((ball‘𝐷)‘⟨(1st ‘(𝐹𝑘)), (2nd ‘(𝐹𝑘))⟩))
54 df-ov 7145 . . . . 5 ((1st ‘(𝐹𝑘))(ball‘𝐷)(2nd ‘(𝐹𝑘))) = ((ball‘𝐷)‘⟨(1st ‘(𝐹𝑘)), (2nd ‘(𝐹𝑘))⟩)
5553, 54eqtr4di 2851 . . . 4 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((ball‘𝐷)‘(𝐹𝑘)) = ((1st ‘(𝐹𝑘))(ball‘𝐷)(2nd ‘(𝐹𝑘))))
5648, 50, 553eltr4d 2905 . . 3 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((1st𝐹)‘𝑘) ∈ ((ball‘𝐷)‘(𝐹𝑘)))
5736, 56sseldd 3917 . 2 (((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝐴)) → ((1st𝐹)‘𝑘) ∈ ((ball‘𝐷)‘(𝐹𝐴)))
5839ffvelrnda 6835 . . . . . . 7 ((𝜑𝐴 ∈ ℕ) → (𝐹𝐴) ∈ (𝑋 × ℝ+))
59583adant2 1128 . . . . . 6 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (𝐹𝐴) ∈ (𝑋 × ℝ+))
60 1st2nd2 7720 . . . . . 6 ((𝐹𝐴) ∈ (𝑋 × ℝ+) → (𝐹𝐴) = ⟨(1st ‘(𝐹𝐴)), (2nd ‘(𝐹𝐴))⟩)
6159, 60syl 17 . . . . 5 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (𝐹𝐴) = ⟨(1st ‘(𝐹𝐴)), (2nd ‘(𝐹𝐴))⟩)
6261fveq2d 6656 . . . 4 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝐴)) = ((ball‘𝐷)‘⟨(1st ‘(𝐹𝐴)), (2nd ‘(𝐹𝐴))⟩))
63 df-ov 7145 . . . 4 ((1st ‘(𝐹𝐴))(ball‘𝐷)(2nd ‘(𝐹𝐴))) = ((ball‘𝐷)‘⟨(1st ‘(𝐹𝐴)), (2nd ‘(𝐹𝐴))⟩)
6462, 63eqtr4di 2851 . . 3 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝐴)) = ((1st ‘(𝐹𝐴))(ball‘𝐷)(2nd ‘(𝐹𝐴))))
65 xp1st 7713 . . . . 5 ((𝐹𝐴) ∈ (𝑋 × ℝ+) → (1st ‘(𝐹𝐴)) ∈ 𝑋)
6659, 65syl 17 . . . 4 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (1st ‘(𝐹𝐴)) ∈ 𝑋)
67 xp2nd 7714 . . . . . 6 ((𝐹𝐴) ∈ (𝑋 × ℝ+) → (2nd ‘(𝐹𝐴)) ∈ ℝ+)
6859, 67syl 17 . . . . 5 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (2nd ‘(𝐹𝐴)) ∈ ℝ+)
6968rpxrd 12437 . . . 4 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → (2nd ‘(𝐹𝐴)) ∈ ℝ*)
70 blssm 23063 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝐹𝐴)) ∈ 𝑋 ∧ (2nd ‘(𝐹𝐴)) ∈ ℝ*) → ((1st ‘(𝐹𝐴))(ball‘𝐷)(2nd ‘(𝐹𝐴))) ⊆ 𝑋)
713, 66, 69, 70syl3anc 1368 . . 3 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → ((1st ‘(𝐹𝐴))(ball‘𝐷)(2nd ‘(𝐹𝐴))) ⊆ 𝑋)
7264, 71eqsstrd 3954 . 2 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → ((ball‘𝐷)‘(𝐹𝐴)) ⊆ 𝑋)
731, 6, 8, 9, 57, 72lmcls 21945 1 ((𝜑 ∧ (1st𝐹)(⇝𝑡𝐽)𝑃𝐴 ∈ ℕ) → 𝑃 ∈ ((cls‘𝐽)‘((ball‘𝐷)‘(𝐹𝐴))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ⊆ wss 3882  ⟨cop 4533   class class class wbr 5033   × cxp 5520   ∘ ccom 5526  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142  1st c1st 7679  2nd c2nd 7680  1c1 10542   + caddc 10544  ℝ*cxr 10678  ℕcn 11640  ℤcz 11986  ℤ≥cuz 12248  ℝ+crp 12394  ∞Metcxmet 20094  ballcbl 20096  MetOpencmopn 20099  TopOnctopon 21553  clsccl 21661  ⇝𝑡clm 21869 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-rep 5157  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  ax-pre-sup 10619 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-rmo 3114  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-er 8287  df-map 8406  df-pm 8407  df-en 8508  df-dom 8509  df-sdom 8510  df-sup 8905  df-inf 8906  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-div 11302  df-nn 11641  df-2 11703  df-n0 11901  df-z 11987  df-uz 12249  df-q 12354  df-rp 12395  df-xneg 12512  df-xadd 12513  df-xmul 12514  df-topgen 16726  df-psmet 20101  df-xmet 20102  df-bl 20104  df-mopn 20105  df-top 21537  df-topon 21554  df-bases 21589  df-cld 21662  df-ntr 21663  df-cls 21664  df-lm 21872 This theorem is referenced by:  bcthlem3  23968  heiborlem8  35323
 Copyright terms: Public domain W3C validator