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

Theorem kqnrmlem2 21826
Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
Assertion
Ref Expression
kqnrmlem2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm)
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem kqnrmlem2
Dummy variables 𝑚 𝑤 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 20996 . . 3 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
21adantr 472 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Top)
3 simplr 785 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (KQ‘𝐽) ∈ Nrm)
4 simpll 783 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝐽 ∈ (TopOn‘𝑋))
5 simprl 787 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑧𝐽)
6 kqval.2 . . . . . . 7 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
76kqopn 21816 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → (𝐹𝑧) ∈ (KQ‘𝐽))
84, 5, 7syl2anc 579 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹𝑧) ∈ (KQ‘𝐽))
9 inss1 3991 . . . . . . 7 ((Clsd‘𝐽) ∩ 𝒫 𝑧) ⊆ (Clsd‘𝐽)
10 simprr 789 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))
119, 10sseldi 3758 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘𝐽))
126kqcld 21817 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ (Clsd‘𝐽)) → (𝐹𝑤) ∈ (Clsd‘(KQ‘𝐽)))
134, 11, 12syl2anc 579 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹𝑤) ∈ (Clsd‘(KQ‘𝐽)))
14 inss2 3992 . . . . . . 7 ((Clsd‘𝐽) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
1514, 10sseldi 3758 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
16 elpwi 4324 . . . . . 6 (𝑤 ∈ 𝒫 𝑧𝑤𝑧)
17 imass2 5682 . . . . . 6 (𝑤𝑧 → (𝐹𝑤) ⊆ (𝐹𝑧))
1815, 16, 173syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹𝑤) ⊆ (𝐹𝑧))
19 nrmsep3 21438 . . . . 5 (((KQ‘𝐽) ∈ Nrm ∧ ((𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹𝑤) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑤) ⊆ (𝐹𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))
203, 8, 13, 18, 19syl13anc 1491 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))
21 simplll 791 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
226kqid 21810 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
2321, 22syl 17 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
24 simprl 787 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑚 ∈ (KQ‘𝐽))
25 cnima 21348 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑚 ∈ (KQ‘𝐽)) → (𝐹𝑚) ∈ 𝐽)
2623, 24, 25syl2anc 579 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹𝑚) ∈ 𝐽)
27 simprrl 799 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹𝑤) ⊆ 𝑚)
286kqffn 21807 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
29 fnfun 6165 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
3021, 28, 293syl 18 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → Fun 𝐹)
3111adantr 472 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑤 ∈ (Clsd‘𝐽))
32 eqid 2764 . . . . . . . . . 10 𝐽 = 𝐽
3332cldss 21112 . . . . . . . . 9 (𝑤 ∈ (Clsd‘𝐽) → 𝑤 𝐽)
3431, 33syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑤 𝐽)
35 fndm 6167 . . . . . . . . . 10 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
3621, 28, 353syl 18 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝑋)
37 toponuni 20997 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
3821, 37syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑋 = 𝐽)
3936, 38eqtrd 2798 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → dom 𝐹 = 𝐽)
4034, 39sseqtr4d 3801 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ dom 𝐹)
41 funimass3 6522 . . . . . . 7 ((Fun 𝐹𝑤 ⊆ dom 𝐹) → ((𝐹𝑤) ⊆ 𝑚𝑤 ⊆ (𝐹𝑚)))
4230, 40, 41syl2anc 579 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ((𝐹𝑤) ⊆ 𝑚𝑤 ⊆ (𝐹𝑚)))
4327, 42mpbid 223 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑤 ⊆ (𝐹𝑚))
446kqtopon 21809 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
45 topontop 20996 . . . . . . . . . 10 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
4621, 44, 453syl 18 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (KQ‘𝐽) ∈ Top)
47 elssuni 4624 . . . . . . . . . 10 (𝑚 ∈ (KQ‘𝐽) → 𝑚 (KQ‘𝐽))
4847ad2antrl 719 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑚 (KQ‘𝐽))
49 eqid 2764 . . . . . . . . . 10 (KQ‘𝐽) = (KQ‘𝐽)
5049clscld 21130 . . . . . . . . 9 (((KQ‘𝐽) ∈ Top ∧ 𝑚 (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
5146, 48, 50syl2anc 579 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
52 cnclima 21351 . . . . . . . 8 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
5323, 51, 52syl2anc 579 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
5449sscls 21139 . . . . . . . . 9 (((KQ‘𝐽) ∈ Top ∧ 𝑚 (KQ‘𝐽)) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
5546, 48, 54syl2anc 579 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
56 imass2 5682 . . . . . . . 8 (𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚) → (𝐹𝑚) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
5755, 56syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹𝑚) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
5832clsss2 21155 . . . . . . 7 (((𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽) ∧ (𝐹𝑚) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) → ((cls‘𝐽)‘(𝐹𝑚)) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
5953, 57, 58syl2anc 579 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘(𝐹𝑚)) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
60 simprrr 800 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧))
61 imass2 5682 . . . . . . . 8 (((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (𝐹 “ (𝐹𝑧)))
6260, 61syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (𝐹 “ (𝐹𝑧)))
635adantr 472 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → 𝑧𝐽)
646kqsat 21813 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → (𝐹 “ (𝐹𝑧)) = 𝑧)
6521, 63, 64syl2anc 579 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹 “ (𝐹𝑧)) = 𝑧)
6662, 65sseqtrd 3800 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ 𝑧)
6759, 66sstrd 3770 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘(𝐹𝑚)) ⊆ 𝑧)
68 sseq2 3786 . . . . . . 7 (𝑢 = (𝐹𝑚) → (𝑤𝑢𝑤 ⊆ (𝐹𝑚)))
69 fveq2 6374 . . . . . . . 8 (𝑢 = (𝐹𝑚) → ((cls‘𝐽)‘𝑢) = ((cls‘𝐽)‘(𝐹𝑚)))
7069sseq1d 3791 . . . . . . 7 (𝑢 = (𝐹𝑚) → (((cls‘𝐽)‘𝑢) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(𝐹𝑚)) ⊆ 𝑧))
7168, 70anbi12d 624 . . . . . 6 (𝑢 = (𝐹𝑚) → ((𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹𝑚) ∧ ((cls‘𝐽)‘(𝐹𝑚)) ⊆ 𝑧)))
7271rspcev 3460 . . . . 5 (((𝐹𝑚) ∈ 𝐽 ∧ (𝑤 ⊆ (𝐹𝑚) ∧ ((cls‘𝐽)‘(𝐹𝑚)) ⊆ 𝑧)) → ∃𝑢𝐽 (𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
7326, 43, 67, 72syl12anc 865 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹𝑧)))) → ∃𝑢𝐽 (𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
7420, 73rexlimddv 3181 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑢𝐽 (𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
7574ralrimivva 3117 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → ∀𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢𝐽 (𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
76 isnrm 21418 . 2 (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑧𝐽𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢𝐽 (𝑤𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)))
772, 75, 76sylanbrc 578 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3054  wrex 3055  {crab 3058  cin 3730  wss 3731  𝒫 cpw 4314   cuni 4593  cmpt 4887  ccnv 5275  dom cdm 5276  ran crn 5277  cima 5279  Fun wfun 6061   Fn wfn 6062  cfv 6067  (class class class)co 6841  Topctop 20976  TopOnctopon 20993  Clsdccld 21099  clsccl 21101   Cn ccn 21307  Nrmcnrm 21393  KQckq 21775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-map 8061  df-qtop 16434  df-top 20977  df-topon 20994  df-cld 21102  df-cls 21104  df-cn 21310  df-nrm 21400  df-kq 21776
This theorem is referenced by:  kqnrm  21834
  Copyright terms: Public domain W3C validator