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

Theorem pnrmopn 21867
Description: An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
pnrmopn ((𝐽 ∈ PNrm ∧ 𝐴𝐽) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ran 𝑓)
Distinct variable groups:   𝐴,𝑓   𝑓,𝐽

Proof of Theorem pnrmopn
Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pnrmtop 21865 . . . 4 (𝐽 ∈ PNrm → 𝐽 ∈ Top)
2 eqid 2824 . . . . 5 𝐽 = 𝐽
32opncld 21557 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝐽) → ( 𝐽𝐴) ∈ (Clsd‘𝐽))
41, 3sylan 580 . . 3 ((𝐽 ∈ PNrm ∧ 𝐴𝐽) → ( 𝐽𝐴) ∈ (Clsd‘𝐽))
5 pnrmcld 21866 . . 3 ((𝐽 ∈ PNrm ∧ ( 𝐽𝐴) ∈ (Clsd‘𝐽)) → ∃𝑔 ∈ (𝐽m ℕ)( 𝐽𝐴) = ran 𝑔)
64, 5syldan 591 . 2 ((𝐽 ∈ PNrm ∧ 𝐴𝐽) → ∃𝑔 ∈ (𝐽m ℕ)( 𝐽𝐴) = ran 𝑔)
71ad2antrr 722 . . . . . . . 8 (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) ∧ 𝑥 ∈ ℕ) → 𝐽 ∈ Top)
8 elmapi 8421 . . . . . . . . . 10 (𝑔 ∈ (𝐽m ℕ) → 𝑔:ℕ⟶𝐽)
98adantl 482 . . . . . . . . 9 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → 𝑔:ℕ⟶𝐽)
109ffvelrnda 6846 . . . . . . . 8 (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) ∧ 𝑥 ∈ ℕ) → (𝑔𝑥) ∈ 𝐽)
112opncld 21557 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔𝑥) ∈ 𝐽) → ( 𝐽 ∖ (𝑔𝑥)) ∈ (Clsd‘𝐽))
127, 10, 11syl2anc 584 . . . . . . 7 (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) ∧ 𝑥 ∈ ℕ) → ( 𝐽 ∖ (𝑔𝑥)) ∈ (Clsd‘𝐽))
1312fmpttd 6874 . . . . . 6 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))):ℕ⟶(Clsd‘𝐽))
14 fvex 6679 . . . . . . 7 (Clsd‘𝐽) ∈ V
15 nnex 11636 . . . . . . 7 ℕ ∈ V
1614, 15elmap 8428 . . . . . 6 ((𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) ∈ ((Clsd‘𝐽) ↑m ℕ) ↔ (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))):ℕ⟶(Clsd‘𝐽))
1713, 16sylibr 235 . . . . 5 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) ∈ ((Clsd‘𝐽) ↑m ℕ))
18 iundif2 4992 . . . . . . 7 𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) = ( 𝐽 𝑥 ∈ ℕ (𝑔𝑥))
19 ffn 6510 . . . . . . . . 9 (𝑔:ℕ⟶𝐽𝑔 Fn ℕ)
20 fniinfv 6738 . . . . . . . . 9 (𝑔 Fn ℕ → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
219, 19, 203syl 18 . . . . . . . 8 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
2221difeq2d 4102 . . . . . . 7 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → ( 𝐽 𝑥 ∈ ℕ (𝑔𝑥)) = ( 𝐽 ran 𝑔))
2318, 22syl5eq 2872 . . . . . 6 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → 𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) = ( 𝐽 ran 𝑔))
24 uniexg 7460 . . . . . . . . . . 11 (𝐽 ∈ PNrm → 𝐽 ∈ V)
25 difexg 5227 . . . . . . . . . . 11 ( 𝐽 ∈ V → ( 𝐽 ∖ (𝑔𝑥)) ∈ V)
2624, 25syl 17 . . . . . . . . . 10 (𝐽 ∈ PNrm → ( 𝐽 ∖ (𝑔𝑥)) ∈ V)
2726ralrimivw 3187 . . . . . . . . 9 (𝐽 ∈ PNrm → ∀𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) ∈ V)
2827adantr 481 . . . . . . . 8 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → ∀𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) ∈ V)
29 dfiun2g 4951 . . . . . . . 8 (∀𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) ∈ V → 𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) = {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = ( 𝐽 ∖ (𝑔𝑥))})
3028, 29syl 17 . . . . . . 7 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → 𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) = {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = ( 𝐽 ∖ (𝑔𝑥))})
31 eqid 2824 . . . . . . . . 9 (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) = (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥)))
3231rnmpt 5825 . . . . . . . 8 ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) = {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = ( 𝐽 ∖ (𝑔𝑥))}
3332unieqi 4845 . . . . . . 7 ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) = {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = ( 𝐽 ∖ (𝑔𝑥))}
3430, 33syl6eqr 2878 . . . . . 6 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → 𝑥 ∈ ℕ ( 𝐽 ∖ (𝑔𝑥)) = ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))))
3523, 34eqtr3d 2862 . . . . 5 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → ( 𝐽 ran 𝑔) = ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))))
36 rneq 5804 . . . . . . 7 (𝑓 = (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) → ran 𝑓 = ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))))
3736unieqd 4846 . . . . . 6 (𝑓 = (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) → ran 𝑓 = ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))))
3837rspceeqv 3641 . . . . 5 (((𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥))) ∈ ((Clsd‘𝐽) ↑m ℕ) ∧ ( 𝐽 ran 𝑔) = ran (𝑥 ∈ ℕ ↦ ( 𝐽 ∖ (𝑔𝑥)))) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)( 𝐽 ran 𝑔) = ran 𝑓)
3917, 35, 38syl2anc 584 . . . 4 ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽m ℕ)) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)( 𝐽 ran 𝑔) = ran 𝑓)
4039ad2ant2r 743 . . 3 (((𝐽 ∈ PNrm ∧ 𝐴𝐽) ∧ (𝑔 ∈ (𝐽m ℕ) ∧ ( 𝐽𝐴) = ran 𝑔)) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)( 𝐽 ran 𝑔) = ran 𝑓)
41 difeq2 4096 . . . . . . . 8 (( 𝐽𝐴) = ran 𝑔 → ( 𝐽 ∖ ( 𝐽𝐴)) = ( 𝐽 ran 𝑔))
4241eqcomd 2830 . . . . . . 7 (( 𝐽𝐴) = ran 𝑔 → ( 𝐽 ran 𝑔) = ( 𝐽 ∖ ( 𝐽𝐴)))
43 elssuni 4865 . . . . . . . 8 (𝐴𝐽𝐴 𝐽)
44 dfss4 4238 . . . . . . . 8 (𝐴 𝐽 ↔ ( 𝐽 ∖ ( 𝐽𝐴)) = 𝐴)
4543, 44sylib 219 . . . . . . 7 (𝐴𝐽 → ( 𝐽 ∖ ( 𝐽𝐴)) = 𝐴)
4642, 45sylan9eqr 2882 . . . . . 6 ((𝐴𝐽 ∧ ( 𝐽𝐴) = ran 𝑔) → ( 𝐽 ran 𝑔) = 𝐴)
4746ad2ant2l 742 . . . . 5 (((𝐽 ∈ PNrm ∧ 𝐴𝐽) ∧ (𝑔 ∈ (𝐽m ℕ) ∧ ( 𝐽𝐴) = ran 𝑔)) → ( 𝐽 ran 𝑔) = 𝐴)
4847eqeq1d 2826 . . . 4 (((𝐽 ∈ PNrm ∧ 𝐴𝐽) ∧ (𝑔 ∈ (𝐽m ℕ) ∧ ( 𝐽𝐴) = ran 𝑔)) → (( 𝐽 ran 𝑔) = ran 𝑓𝐴 = ran 𝑓))
4948rexbidv 3301 . . 3 (((𝐽 ∈ PNrm ∧ 𝐴𝐽) ∧ (𝑔 ∈ (𝐽m ℕ) ∧ ( 𝐽𝐴) = ran 𝑔)) → (∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)( 𝐽 ran 𝑔) = ran 𝑓 ↔ ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ran 𝑓))
5040, 49mpbid 233 . 2 (((𝐽 ∈ PNrm ∧ 𝐴𝐽) ∧ (𝑔 ∈ (𝐽m ℕ) ∧ ( 𝐽𝐴) = ran 𝑔)) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ran 𝑓)
516, 50rexlimddv 3295 1 ((𝐽 ∈ PNrm ∧ 𝐴𝐽) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ran 𝑓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2106  {cab 2802  wral 3142  wrex 3143  Vcvv 3499  cdif 3936  wss 3939   cuni 4836   cint 4873   ciun 4916   ciin 4917  cmpt 5142  ran crn 5554   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  m cmap 8399  cn 11630  Topctop 21417  Clsdccld 21540  PNrmcpnrm 21836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-1cn 10587  ax-addcl 10589
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-map 8401  df-nn 11631  df-top 21418  df-cld 21543  df-nrm 21841  df-pnrm 21843
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator