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

Theorem kqnrmlem1 21459
 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 21443 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
32adantr 481 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4 topontop 20640 . . 3 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Top)
6 simplr 791 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐽 ∈ Nrm)
71kqid 21444 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
87ad2antrr 761 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
9 simprl 793 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑧 ∈ (KQ‘𝐽))
10 cnima 20982 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑧 ∈ (KQ‘𝐽)) → (𝐹𝑧) ∈ 𝐽)
118, 9, 10syl2anc 692 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑧) ∈ 𝐽)
12 inss1 3813 . . . . . . 7 ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧) ⊆ (Clsd‘(KQ‘𝐽))
13 simprr 795 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))
1412, 13sseldi 3582 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
15 cnclima 20985 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑤 ∈ (Clsd‘(KQ‘𝐽))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
168, 14, 15syl2anc 692 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
17 inss2 3814 . . . . . . 7 ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
1817, 13sseldi 3582 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
19 elpwi 4142 . . . . . 6 (𝑤 ∈ 𝒫 𝑧𝑤𝑧)
20 imass2 5462 . . . . . 6 (𝑤𝑧 → (𝐹𝑤) ⊆ (𝐹𝑧))
2118, 19, 203syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ⊆ (𝐹𝑧))
22 nrmsep3 21072 . . . . 5 ((𝐽 ∈ Nrm ∧ ((𝐹𝑧) ∈ 𝐽 ∧ (𝐹𝑤) ∈ (Clsd‘𝐽) ∧ (𝐹𝑤) ⊆ (𝐹𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
236, 11, 16, 21, 22syl13anc 1325 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
24 simplll 797 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
25 simprl 793 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢𝐽)
261kqopn 21450 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢𝐽) → (𝐹𝑢) ∈ (KQ‘𝐽))
2724, 25, 26syl2anc 692 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ∈ (KQ‘𝐽))
28 simprrl 803 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑤) ⊆ 𝑢)
291kqffn 21441 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
30 fnfun 5948 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
3124, 29, 303syl 18 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → Fun 𝐹)
3214adantr 481 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
33 eqid 2621 . . . . . . . . . 10 (KQ‘𝐽) = (KQ‘𝐽)
3433cldss 20746 . . . . . . . . 9 (𝑤 ∈ (Clsd‘(KQ‘𝐽)) → 𝑤 (KQ‘𝐽))
3532, 34syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 (KQ‘𝐽))
36 toponuni 20641 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3724, 2, 363syl 18 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ran 𝐹 = (KQ‘𝐽))
3835, 37sseqtr4d 3623 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ ran 𝐹)
39 funimass1 5931 . . . . . . 7 ((Fun 𝐹𝑤 ⊆ ran 𝐹) → ((𝐹𝑤) ⊆ 𝑢𝑤 ⊆ (𝐹𝑢)))
4031, 38, 39syl2anc 692 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((𝐹𝑤) ⊆ 𝑢𝑤 ⊆ (𝐹𝑢)))
4128, 40mpd 15 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ (𝐹𝑢))
42 topontop 20640 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4324, 42syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ Top)
44 elssuni 4435 . . . . . . . . . 10 (𝑢𝐽𝑢 𝐽)
4544ad2antrl 763 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 𝐽)
46 eqid 2621 . . . . . . . . . 10 𝐽 = 𝐽
4746clscld 20764 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
4843, 45, 47syl2anc 692 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
491kqcld 21451 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
5024, 48, 49syl2anc 692 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
5146sscls 20773 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
5243, 45, 51syl2anc 692 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
53 imass2 5462 . . . . . . . 8 (𝑢 ⊆ ((cls‘𝐽)‘𝑢) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5452, 53syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5533clsss2 20789 . . . . . . 7 (((𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5650, 54, 55syl2anc 692 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
57 simprrr 804 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧))
5846clsss3 20776 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
5943, 45, 58syl2anc 692 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
60 fndm 5950 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
6124, 29, 603syl 18 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝑋)
62 toponuni 20641 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
6324, 62syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑋 = 𝐽)
6461, 63eqtrd 2655 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝐽)
6559, 64sseqtr4d 3623 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹)
66 funimass3 6291 . . . . . . . 8 ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
6731, 65, 66syl2anc 692 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
6857, 67mpbird 247 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧)
6956, 68sstrd 3594 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)
70 sseq2 3608 . . . . . . 7 (𝑚 = (𝐹𝑢) → (𝑤𝑚𝑤 ⊆ (𝐹𝑢)))
71 fveq2 6150 . . . . . . . 8 (𝑚 = (𝐹𝑢) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹𝑢)))
7271sseq1d 3613 . . . . . . 7 (𝑚 = (𝐹𝑢) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧 ↔ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧))
7370, 72anbi12d 746 . . . . . 6 (𝑚 = (𝐹𝑢) → ((𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)))
7473rspcev 3295 . . . . 5 (((𝐹𝑢) ∈ (KQ‘𝐽) ∧ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7527, 41, 69, 74syl12anc 1321 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7623, 75rexlimddv 3028 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7776ralrimivva 2965 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
78 isnrm 21052 . 2 ((KQ‘𝐽) ∈ Nrm ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧)))
795, 77, 78sylanbrc 697 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  {crab 2911   ∩ cin 3555   ⊆ wss 3556  𝒫 cpw 4132  ∪ cuni 4404   ↦ cmpt 4675  ◡ccnv 5075  dom cdm 5076  ran crn 5077   “ cima 5079  Fun wfun 5843   Fn wfn 5844  ‘cfv 5849  (class class class)co 6607  Topctop 20620  TopOnctopon 20637  Clsdccld 20733  clsccl 20735   Cn ccn 20941  Nrmcnrm 21027  KQckq 21409 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-map 7807  df-qtop 16091  df-top 20621  df-topon 20638  df-cld 20736  df-cls 20738  df-cn 20944  df-nrm 21034  df-kq 21410 This theorem is referenced by:  kqnrm  21468
 Copyright terms: Public domain W3C validator