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