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

Theorem kqnrmlem1 22894
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 22878 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
32adantr 481 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4 topontop 22062 . . 3 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Top)
6 simplr 766 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐽 ∈ Nrm)
71kqid 22879 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
87ad2antrr 723 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
9 simprl 768 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑧 ∈ (KQ‘𝐽))
10 cnima 22416 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑧 ∈ (KQ‘𝐽)) → (𝐹𝑧) ∈ 𝐽)
118, 9, 10syl2anc 584 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑧) ∈ 𝐽)
12 simprr 770 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))
1312elin1d 4132 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
14 cnclima 22419 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑤 ∈ (Clsd‘(KQ‘𝐽))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
158, 13, 14syl2anc 584 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ∈ (Clsd‘𝐽))
1612elin2d 4133 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
17 elpwi 4542 . . . . . 6 (𝑤 ∈ 𝒫 𝑧𝑤𝑧)
18 imass2 6010 . . . . . 6 (𝑤𝑧 → (𝐹𝑤) ⊆ (𝐹𝑧))
1916, 17, 183syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (𝐹𝑤) ⊆ (𝐹𝑧))
20 nrmsep3 22506 . . . . 5 ((𝐽 ∈ Nrm ∧ ((𝐹𝑧) ∈ 𝐽 ∧ (𝐹𝑤) ∈ (Clsd‘𝐽) ∧ (𝐹𝑤) ⊆ (𝐹𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
216, 11, 15, 19, 20syl13anc 1371 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑢𝐽 ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))
22 simplll 772 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
23 simprl 768 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢𝐽)
241kqopn 22885 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢𝐽) → (𝐹𝑢) ∈ (KQ‘𝐽))
2522, 23, 24syl2anc 584 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ∈ (KQ‘𝐽))
26 simprrl 778 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑤) ⊆ 𝑢)
271kqffn 22876 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
28 fnfun 6533 . . . . . . . 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 2738 . . . . . . . . . 10 (KQ‘𝐽) = (KQ‘𝐽)
3231cldss 22180 . . . . . . . . 9 (𝑤 ∈ (Clsd‘(KQ‘𝐽)) → 𝑤 (KQ‘𝐽))
3330, 32syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 (KQ‘𝐽))
34 toponuni 22063 . . . . . . . . 9 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3522, 2, 343syl 18 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ran 𝐹 = (KQ‘𝐽))
3633, 35sseqtrrd 3962 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ ran 𝐹)
37 funimass1 6516 . . . . . . 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 22062 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4122, 40syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝐽 ∈ Top)
42 elssuni 4871 . . . . . . . . . 10 (𝑢𝐽𝑢 𝐽)
4342ad2antrl 725 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 𝐽)
44 eqid 2738 . . . . . . . . . 10 𝐽 = 𝐽
4544clscld 22198 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
4641, 43, 45syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
471kqcld 22886 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
4822, 46, 47syl2anc 584 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
4944sscls 22207 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
5041, 43, 49syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
51 imass2 6010 . . . . . . . 8 (𝑢 ⊆ ((cls‘𝐽)‘𝑢) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5250, 51syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5331clsss2 22223 . . . . . . 7 (((𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
5448, 52, 53syl2anc 584 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
55 simprrr 779 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧))
5644clsss3 22210 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑢 𝐽) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
5741, 43, 56syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ 𝐽)
58 fndm 6536 . . . . . . . . . . 11 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
5922, 27, 583syl 18 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝑋)
60 toponuni 22063 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
6122, 60syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → 𝑋 = 𝐽)
6259, 61eqtrd 2778 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝐽)
6357, 62sseqtrrd 3962 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹)
64 funimass3 6931 . . . . . . . 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 3931 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)
68 sseq2 3947 . . . . . . 7 (𝑚 = (𝐹𝑢) → (𝑤𝑚𝑤 ⊆ (𝐹𝑢)))
69 fveq2 6774 . . . . . . . 8 (𝑚 = (𝐹𝑢) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹𝑢)))
7069sseq1d 3952 . . . . . . 7 (𝑚 = (𝐹𝑢) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧 ↔ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧))
7168, 70anbi12d 631 . . . . . 6 (𝑚 = (𝐹𝑢) → ((𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)))
7271rspcev 3561 . . . . 5 (((𝐹𝑢) ∈ (KQ‘𝐽) ∧ (𝑤 ⊆ (𝐹𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑢)) ⊆ 𝑧)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7325, 39, 67, 72syl12anc 834 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢𝐽 ∧ ((𝐹𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (𝐹𝑧)))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7421, 73rexlimddv 3220 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
7574ralrimivva 3123 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
76 isnrm 22486 . 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 1539  wcel 2106  wral 3064  wrex 3065  {crab 3068  cin 3886  wss 3887  𝒫 cpw 4533   cuni 4839  cmpt 5157  ccnv 5588  dom cdm 5589  ran crn 5590  cima 5592  Fun wfun 6427   Fn wfn 6428  cfv 6433  (class class class)co 7275  Topctop 22042  TopOnctopon 22059  Clsdccld 22167  clsccl 22169   Cn ccn 22375  Nrmcnrm 22461  KQckq 22844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-map 8617  df-qtop 17218  df-top 22043  df-topon 22060  df-cld 22170  df-cls 22172  df-cn 22378  df-nrm 22468  df-kq 22845
This theorem is referenced by:  kqnrm  22903
  Copyright terms: Public domain W3C validator