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

Theorem kqnrmlem1 21768
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 21752 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
32adantr 468 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4 topontop 20939 . . 3 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Top)
6 simplr 776 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐽 ∈ Nrm)
71kqid 21753 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
87ad2antrr 708 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
9 simprl 778 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑧 ∈ (KQ‘𝐽))
10 cnima 21291 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑧 ∈ (KQ‘𝐽)) → (𝐹𝑧) ∈ 𝐽)
118, 9, 10syl2anc 575 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑧) ∈ 𝐽)
12 inss1 4040 . . . . . . 7 ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧) ⊆ (Clsd‘(KQ‘𝐽))
13 simprr 780 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))
1412, 13sseldi 3807 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
15 cnclima 21294 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑤 ∈ (Clsd‘(KQ‘𝐽))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
168, 14, 15syl2anc 575 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
17 inss2 4041 . . . . . . 7 ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
1817, 13sseldi 3807 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
19 elpwi 4372 . . . . . 6 (𝑤 ∈ 𝒫 𝑧𝑤𝑧)
20 imass2 5722 . . . . . 6 (𝑤𝑧 → (𝐹𝑤) ⊆ (𝐹𝑧))
2118, 19, 203syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ⊆ (𝐹𝑧))
22 nrmsep3 21381 . . . . 5 ((𝐽 ∈ Nrm ∧ ((𝐹𝑧) ∈ 𝐽 ∧ (𝐹𝑤) ∈ (Clsd‘𝐽) ∧ (𝐹𝑤) ⊆ (𝐹𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
236, 11, 16, 21, 22syl13anc 1484 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
24 simplll 782 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
25 simprl 778 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢𝐽)
261kqopn 21759 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢𝐽) → (𝐹𝑢) ∈ (KQ‘𝐽))
2724, 25, 26syl2anc 575 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ∈ (KQ‘𝐽))
28 simprrl 790 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑤) ⊆ 𝑢)
291kqffn 21750 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
30 fnfun 6206 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
3124, 29, 303syl 18 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → Fun 𝐹)
3214adantr 468 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
33 eqid 2817 . . . . . . . . . 10 (KQ‘𝐽) = (KQ‘𝐽)
3433cldss 21055 . . . . . . . . 9 (𝑤 ∈ (Clsd‘(KQ‘𝐽)) → 𝑤 (KQ‘𝐽))
3532, 34syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 (KQ‘𝐽))
36 toponuni 20940 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3724, 2, 363syl 18 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ran 𝐹 = (KQ‘𝐽))
3835, 37sseqtr4d 3850 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ ran 𝐹)
39 funimass1 6189 . . . . . . 7 ((Fun 𝐹𝑤 ⊆ ran 𝐹) → ((𝐹𝑤) ⊆ 𝑢𝑤 ⊆ (𝐹𝑢)))
4031, 38, 39syl2anc 575 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((𝐹𝑤) ⊆ 𝑢𝑤 ⊆ (𝐹𝑢)))
4128, 40mpd 15 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ (𝐹𝑢))
42 topontop 20939 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4324, 42syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ Top)
44 elssuni 4672 . . . . . . . . . 10 (𝑢𝐽𝑢 𝐽)
4544ad2antrl 710 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 𝐽)
46 eqid 2817 . . . . . . . . . 10 𝐽 = 𝐽
4746clscld 21073 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
4843, 45, 47syl2anc 575 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
491kqcld 21760 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
5024, 48, 49syl2anc 575 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
5146sscls 21082 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
5243, 45, 51syl2anc 575 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
53 imass2 5722 . . . . . . . 8 (𝑢 ⊆ ((cls‘𝐽)‘𝑢) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5452, 53syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5533clsss2 21098 . . . . . . 7 (((𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5650, 54, 55syl2anc 575 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
57 simprrr 791 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧))
5846clsss3 21085 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
5943, 45, 58syl2anc 575 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
60 fndm 6208 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
6124, 29, 603syl 18 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝑋)
62 toponuni 20940 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
6324, 62syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑋 = 𝐽)
6461, 63eqtrd 2851 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝐽)
6559, 64sseqtr4d 3850 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹)
66 funimass3 6562 . . . . . . . 8 ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
6731, 65, 66syl2anc 575 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
6857, 67mpbird 248 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧)
6956, 68sstrd 3819 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)
70 sseq2 3835 . . . . . . 7 (𝑚 = (𝐹𝑢) → (𝑤𝑚𝑤 ⊆ (𝐹𝑢)))
71 fveq2 6415 . . . . . . . 8 (𝑚 = (𝐹𝑢) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹𝑢)))
7271sseq1d 3840 . . . . . . 7 (𝑚 = (𝐹𝑢) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧 ↔ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧))
7370, 72anbi12d 618 . . . . . 6 (𝑚 = (𝐹𝑢) → ((𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)))
7473rspcev 3513 . . . . 5 (((𝐹𝑢) ∈ (KQ‘𝐽) ∧ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7527, 41, 69, 74syl12anc 856 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7623, 75rexlimddv 3234 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7776ralrimivva 3170 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
78 isnrm 21361 . 2 ((KQ‘𝐽) ∈ Nrm ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧)))
795, 77, 78sylanbrc 574 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wral 3107  wrex 3108  {crab 3111  cin 3779  wss 3780  𝒫 cpw 4362   cuni 4641  cmpt 4934  ccnv 5321  dom cdm 5322  ran crn 5323  cima 5325  Fun wfun 6102   Fn wfn 6103  cfv 6108  (class class class)co 6881  Topctop 20919  TopOnctopon 20936  Clsdccld 21042  clsccl 21044   Cn ccn 21250  Nrmcnrm 21336  KQckq 21718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5230  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-map 8101  df-qtop 16379  df-top 20920  df-topon 20937  df-cld 21045  df-cls 21047  df-cn 21253  df-nrm 21343  df-kq 21719
This theorem is referenced by:  kqnrm  21777
  Copyright terms: Public domain W3C validator