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

Theorem rectbntr0 23734
Description: A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.)
Assertion
Ref Expression
rectbntr0 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅)

Proof of Theorem rectbntr0
StepHypRef Expression
1 nnex 11841 . . . 4 ℕ ∈ V
21canth2 8804 . . 3 ℕ ≺ 𝒫 ℕ
3 domnsym 8777 . . 3 (𝒫 ℕ ≼ ℕ → ¬ ℕ ≺ 𝒫 ℕ)
42, 3mt2 203 . 2 ¬ 𝒫 ℕ ≼ ℕ
5 retop 23664 . . . . . 6 (topGen‘ran (,)) ∈ Top
6 simpl 486 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → 𝐴 ⊆ ℝ)
7 uniretop 23665 . . . . . . 7 ℝ = (topGen‘ran (,))
87ntropn 21951 . . . . . 6 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ∈ (topGen‘ran (,)))
95, 6, 8sylancr 590 . . . . 5 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) ∈ (topGen‘ran (,)))
10 opnreen 23733 . . . . . 6 ((((int‘(topGen‘ran (,)))‘𝐴) ∈ (topGen‘ran (,)) ∧ ((int‘(topGen‘ran (,)))‘𝐴) ≠ ∅) → ((int‘(topGen‘ran (,)))‘𝐴) ≈ 𝒫 ℕ)
1110ex 416 . . . . 5 (((int‘(topGen‘ran (,)))‘𝐴) ∈ (topGen‘ran (,)) → (((int‘(topGen‘ran (,)))‘𝐴) ≠ ∅ → ((int‘(topGen‘ran (,)))‘𝐴) ≈ 𝒫 ℕ))
129, 11syl 17 . . . 4 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (((int‘(topGen‘ran (,)))‘𝐴) ≠ ∅ → ((int‘(topGen‘ran (,)))‘𝐴) ≈ 𝒫 ℕ))
13 reex 10825 . . . . . . . 8 ℝ ∈ V
1413ssex 5219 . . . . . . 7 (𝐴 ⊆ ℝ → 𝐴 ∈ V)
157ntrss2 21959 . . . . . . . 8 (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
165, 15mpan 690 . . . . . . 7 (𝐴 ⊆ ℝ → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
17 ssdomg 8679 . . . . . . 7 (𝐴 ∈ V → (((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴 → ((int‘(topGen‘ran (,)))‘𝐴) ≼ 𝐴))
1814, 16, 17sylc 65 . . . . . 6 (𝐴 ⊆ ℝ → ((int‘(topGen‘ran (,)))‘𝐴) ≼ 𝐴)
19 domtr 8686 . . . . . 6 ((((int‘(topGen‘ran (,)))‘𝐴) ≼ 𝐴𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) ≼ ℕ)
2018, 19sylan 583 . . . . 5 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) ≼ ℕ)
21 ensym 8682 . . . . 5 (((int‘(topGen‘ran (,)))‘𝐴) ≈ 𝒫 ℕ → 𝒫 ℕ ≈ ((int‘(topGen‘ran (,)))‘𝐴))
22 endomtr 8691 . . . . . 6 ((𝒫 ℕ ≈ ((int‘(topGen‘ran (,)))‘𝐴) ∧ ((int‘(topGen‘ran (,)))‘𝐴) ≼ ℕ) → 𝒫 ℕ ≼ ℕ)
2322expcom 417 . . . . 5 (((int‘(topGen‘ran (,)))‘𝐴) ≼ ℕ → (𝒫 ℕ ≈ ((int‘(topGen‘ran (,)))‘𝐴) → 𝒫 ℕ ≼ ℕ))
2420, 21, 23syl2im 40 . . . 4 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (((int‘(topGen‘ran (,)))‘𝐴) ≈ 𝒫 ℕ → 𝒫 ℕ ≼ ℕ))
2512, 24syld 47 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (((int‘(topGen‘ran (,)))‘𝐴) ≠ ∅ → 𝒫 ℕ ≼ ℕ))
2625necon1bd 2958 . 2 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (¬ 𝒫 ℕ ≼ ℕ → ((int‘(topGen‘ran (,)))‘𝐴) = ∅))
274, 26mpi 20 1 ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1543  wcel 2110  wne 2940  Vcvv 3413  wss 3871  c0 4242  𝒫 cpw 4518   class class class wbr 5058  ran crn 5557  cfv 6385  cen 8628  cdom 8629  csdm 8630  cr 10733  cn 11835  (,)cioo 12940  topGenctg 16947  Topctop 21795  intcnt 21919
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-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-inf2 9261  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811  ax-pre-sup 10812
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-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-2o 8208  df-oadd 8211  df-omul 8212  df-er 8396  df-map 8515  df-pm 8516  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-sup 9063  df-inf 9064  df-oi 9131  df-card 9560  df-acn 9563  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-div 11495  df-nn 11836  df-2 11898  df-3 11899  df-n0 12096  df-z 12182  df-uz 12444  df-q 12550  df-rp 12592  df-xneg 12709  df-xadd 12710  df-xmul 12711  df-ioo 12944  df-ico 12946  df-icc 12947  df-fz 13101  df-fzo 13244  df-fl 13372  df-seq 13580  df-exp 13641  df-hash 13902  df-cj 14667  df-re 14668  df-im 14669  df-sqrt 14803  df-abs 14804  df-limsup 15037  df-clim 15054  df-rlim 15055  df-sum 15255  df-topgen 16953  df-psmet 20360  df-xmet 20361  df-met 20362  df-bl 20363  df-mopn 20364  df-top 21796  df-topon 21813  df-bases 21848  df-ntr 21922
This theorem is referenced by:  ioonct  42758
  Copyright terms: Public domain W3C validator