MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  kqnrmlem1 Structured version   Visualization version   GIF version
Theorem kqnrmlem1 23238
Description: A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2 𝐹 = (π‘₯ ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ π‘₯ ∈ 𝑦})
Assertion
Ref Expression
kqnrmlem1 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) β†’ (KQβ€˜π½) ∈ Nrm)
Distinct variable groups:   π‘₯,𝑦,𝐽   π‘₯,𝑋,𝑦
Allowed substitution hints:   𝐹(π‘₯,𝑦)
Proof of Theorem kqnrmlem1
Dummy variables π‘š 𝑀 𝑧 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . 5 𝐹 = (π‘₯ ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ π‘₯ ∈ 𝑦})
21kqtopon 23222 . . . 4 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹))
32adantr 481 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) β†’ (KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹))
4 topontop 22406 . . 3 ((KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹) β†’ (KQβ€˜π½) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) β†’ (KQβ€˜π½) ∈ Top)
6 simplr 767 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝐽 ∈ Nrm)
71kqid 23223 . . . . . . 7 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐹 ∈ (𝐽 Cn (KQβ€˜π½)))
87ad2antrr 724 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝐹 ∈ (𝐽 Cn (KQβ€˜π½)))
9 simprl 769 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝑧 ∈ (KQβ€˜π½))
10 cnima 22760 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQβ€˜π½)) ∧ 𝑧 ∈ (KQβ€˜π½)) β†’ (◑𝐹 β€œ 𝑧) ∈ 𝐽)
118, 9, 10syl2anc 584 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ (◑𝐹 β€œ 𝑧) ∈ 𝐽)
12 simprr 771 . . . . . . 7 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))
1312elin1d 4197 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ (Clsdβ€˜(KQβ€˜π½)))
14 cnclima 22763 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQβ€˜π½)) ∧ 𝑀 ∈ (Clsdβ€˜(KQβ€˜π½))) β†’ (◑𝐹 β€œ 𝑀) ∈ (Clsdβ€˜π½))
158, 13, 14syl2anc 584 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ (◑𝐹 β€œ 𝑀) ∈ (Clsdβ€˜π½))
1612elin2d 4198 . . . . . 6 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ 𝒫 𝑧)
17 elpwi 4608 . . . . . 6 (𝑀 ∈ 𝒫 𝑧 β†’ 𝑀 βŠ† 𝑧)
18 imass2 6098 . . . . . 6 (𝑀 βŠ† 𝑧 β†’ (◑𝐹 β€œ 𝑀) βŠ† (◑𝐹 β€œ 𝑧))
1916, 17, 183syl 18 . . . . 5 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ (◑𝐹 β€œ 𝑀) βŠ† (◑𝐹 β€œ 𝑧))
20 nrmsep3 22850 . . . . 5 ((𝐽 ∈ Nrm ∧ ((◑𝐹 β€œ 𝑧) ∈ 𝐽 ∧ (◑𝐹 β€œ 𝑀) ∈ (Clsdβ€˜π½) ∧ (◑𝐹 β€œ 𝑀) βŠ† (◑𝐹 β€œ 𝑧))) β†’ βˆƒπ‘’ ∈ 𝐽 ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))
216, 11, 15, 19, 20syl13anc 1372 . . . 4 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ βˆƒπ‘’ ∈ 𝐽 ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))
22 simplll 773 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
23 simprl 769 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑒 ∈ 𝐽)
241kqopn 23229 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝑒 ∈ 𝐽) β†’ (𝐹 β€œ 𝑒) ∈ (KQβ€˜π½))
2522, 23, 24syl2anc 584 . . . . 5 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ (𝐹 β€œ 𝑒) ∈ (KQβ€˜π½))
26 simprrl 779 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ (◑𝐹 β€œ 𝑀) βŠ† 𝑒)
271kqffn 23220 . . . . . . . 8 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐹 Fn 𝑋)
28 fnfun 6646 . . . . . . . 8 (𝐹 Fn 𝑋 β†’ Fun 𝐹)
2922, 27, 283syl 18 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ Fun 𝐹)
3013adantr 481 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑀 ∈ (Clsdβ€˜(KQβ€˜π½)))
31 eqid 2732 . . . . . . . . . 10 βˆͺ (KQβ€˜π½) = βˆͺ (KQβ€˜π½)
3231cldss 22524 . . . . . . . . 9 (𝑀 ∈ (Clsdβ€˜(KQβ€˜π½)) β†’ 𝑀 βŠ† βˆͺ (KQβ€˜π½))
3330, 32syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑀 βŠ† βˆͺ (KQβ€˜π½))
34 toponuni 22407 . . . . . . . . 9 ((KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹) β†’ ran 𝐹 = βˆͺ (KQβ€˜π½))
3522, 2, 343syl 18 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ran 𝐹 = βˆͺ (KQβ€˜π½))
3633, 35sseqtrrd 4022 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑀 βŠ† ran 𝐹)
37 funimass1 6627 . . . . . . 7 ((Fun 𝐹 ∧ 𝑀 βŠ† ran 𝐹) β†’ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 β†’ 𝑀 βŠ† (𝐹 β€œ 𝑒)))
3829, 36, 37syl2anc 584 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 β†’ 𝑀 βŠ† (𝐹 β€œ 𝑒)))
3926, 38mpd 15 . . . . 5 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑀 βŠ† (𝐹 β€œ 𝑒))
40 topontop 22406 . . . . . . . . . 10 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
4122, 40syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝐽 ∈ Top)
42 elssuni 4940 . . . . . . . . . 10 (𝑒 ∈ 𝐽 β†’ 𝑒 βŠ† βˆͺ 𝐽)
4342ad2antrl 726 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑒 βŠ† βˆͺ 𝐽)
44 eqid 2732 . . . . . . . . . 10 βˆͺ 𝐽 = βˆͺ 𝐽
4544clscld 22542 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑒 βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜π‘’) ∈ (Clsdβ€˜π½))
4641, 43, 45syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜π½)β€˜π‘’) ∈ (Clsdβ€˜π½))
471kqcld 23230 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ ((clsβ€˜π½)β€˜π‘’) ∈ (Clsdβ€˜π½)) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) ∈ (Clsdβ€˜(KQβ€˜π½)))
4822, 46, 47syl2anc 584 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) ∈ (Clsdβ€˜(KQβ€˜π½)))
4944sscls 22551 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑒 βŠ† βˆͺ 𝐽) β†’ 𝑒 βŠ† ((clsβ€˜π½)β€˜π‘’))
5041, 43, 49syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑒 βŠ† ((clsβ€˜π½)β€˜π‘’))
51 imass2 6098 . . . . . . . 8 (𝑒 βŠ† ((clsβ€˜π½)β€˜π‘’) β†’ (𝐹 β€œ 𝑒) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)))
5250, 51syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ (𝐹 β€œ 𝑒) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)))
5331clsss2 22567 . . . . . . 7 (((𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) ∈ (Clsdβ€˜(KQβ€˜π½)) ∧ (𝐹 β€œ 𝑒) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)))
5448, 52, 53syl2anc 584 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)))
55 simprrr 780 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧))
5644clsss3 22554 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑒 βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜π‘’) βŠ† βˆͺ 𝐽)
5741, 43, 56syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜π½)β€˜π‘’) βŠ† βˆͺ 𝐽)
58 fndm 6649 . . . . . . . . . . 11 (𝐹 Fn 𝑋 β†’ dom 𝐹 = 𝑋)
5922, 27, 583syl 18 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ dom 𝐹 = 𝑋)
60 toponuni 22407 . . . . . . . . . . 11 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
6122, 60syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ 𝑋 = βˆͺ 𝐽)
6259, 61eqtrd 2772 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ dom 𝐹 = βˆͺ 𝐽)
6357, 62sseqtrrd 4022 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜π½)β€˜π‘’) βŠ† dom 𝐹)
64 funimass3 7052 . . . . . . . 8 ((Fun 𝐹 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† dom 𝐹) β†’ ((𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) βŠ† 𝑧 ↔ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))
6529, 63, 64syl2anc 584 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) βŠ† 𝑧 ↔ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))
6655, 65mpbird 256 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘’)) βŠ† 𝑧)
6754, 66sstrd 3991 . . . . 5 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑧)
68 sseq2 4007 . . . . . . 7 (π‘š = (𝐹 β€œ 𝑒) β†’ (𝑀 βŠ† π‘š ↔ 𝑀 βŠ† (𝐹 β€œ 𝑒)))
69 fveq2 6888 . . . . . . . 8 (π‘š = (𝐹 β€œ 𝑒) β†’ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) = ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)))
7069sseq1d 4012 . . . . . . 7 (π‘š = (𝐹 β€œ 𝑒) β†’ (((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧 ↔ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑧))
7168, 70anbi12d 631 . . . . . 6 (π‘š = (𝐹 β€œ 𝑒) β†’ ((𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧) ↔ (𝑀 βŠ† (𝐹 β€œ 𝑒) ∧ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑧)))
7271rspcev 3612 . . . . 5 (((𝐹 β€œ 𝑒) ∈ (KQβ€˜π½) ∧ (𝑀 βŠ† (𝐹 β€œ 𝑒) ∧ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑧)) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧))
7325, 39, 67, 72syl12anc 835 . . . 4 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) ∧ (𝑒 ∈ 𝐽 ∧ ((◑𝐹 β€œ 𝑀) βŠ† 𝑒 ∧ ((clsβ€˜π½)β€˜π‘’) βŠ† (◑𝐹 β€œ 𝑧)))) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧))
7421, 73rexlimddv 3161 . . 3 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQβ€˜π½) ∧ 𝑀 ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧))) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧))
7574ralrimivva 3200 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) β†’ βˆ€π‘§ ∈ (KQβ€˜π½)βˆ€π‘€ ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧)βˆƒπ‘š ∈ (KQβ€˜π½)(𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧))
76 isnrm 22830 . 2 ((KQβ€˜π½) ∈ Nrm ↔ ((KQβ€˜π½) ∈ Top ∧ βˆ€π‘§ ∈ (KQβ€˜π½)βˆ€π‘€ ∈ ((Clsdβ€˜(KQβ€˜π½)) ∩ 𝒫 𝑧)βˆƒπ‘š ∈ (KQβ€˜π½)(𝑀 βŠ† π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† 𝑧)))
775, 75, 76sylanbrc 583 1 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Nrm) β†’ (KQβ€˜π½) ∈ Nrm)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  βˆͺ cuni 4907   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6534   Fn wfn 6535  β€˜cfv 6540  (class class class)co 7405  Topctop 22386  TopOnctopon 22403  Clsdccld 22511  clsccl 22513   Cn ccn 22719  Nrmcnrm 22805  KQckq 23188
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8818  df-qtop 17449  df-top 22387  df-topon 22404  df-cld 22514  df-cls 22516  df-cn 22722  df-nrm 22812  df-kq 23189
This theorem is referenced by:  kqnrm  23247
  Copyright terms: Public domain W3C validator