# Metamath Proof Explorer

## Theorem kqnrmlem1

Description: A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 ${⊢}{F}=\left({x}\in {X}⟼\left\{{y}\in {J}|{x}\in {y}\right\}\right)$
Assertion kqnrmlem1 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{Nrm}$

### Proof

Step Hyp Ref Expression
1 kqval.2 ${⊢}{F}=\left({x}\in {X}⟼\left\{{y}\in {J}|{x}\in {y}\right\}\right)$
2 1 kqtopon ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{TopOn}\left(\mathrm{ran}{F}\right)$
3 2 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{TopOn}\left(\mathrm{ran}{F}\right)$
4 topontop ${⊢}\mathrm{KQ}\left({J}\right)\in \mathrm{TopOn}\left(\mathrm{ran}{F}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{Top}$
5 3 4 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{Top}$
6 simplr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {J}\in \mathrm{Nrm}$
7 1 kqid ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {F}\in \left({J}\mathrm{Cn}\mathrm{KQ}\left({J}\right)\right)$
8 7 ad2antrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {F}\in \left({J}\mathrm{Cn}\mathrm{KQ}\left({J}\right)\right)$
9 simprl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {z}\in \mathrm{KQ}\left({J}\right)$
10 cnima ${⊢}\left({F}\in \left({J}\mathrm{Cn}\mathrm{KQ}\left({J}\right)\right)\wedge {z}\in \mathrm{KQ}\left({J}\right)\right)\to {{F}}^{-1}\left[{z}\right]\in {J}$
11 8 9 10 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {{F}}^{-1}\left[{z}\right]\in {J}$
12 simprr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)$
13 12 elin1d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {w}\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)$
14 cnclima ${⊢}\left({F}\in \left({J}\mathrm{Cn}\mathrm{KQ}\left({J}\right)\right)\wedge {w}\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\right)\to {{F}}^{-1}\left[{w}\right]\in \mathrm{Clsd}\left({J}\right)$
15 8 13 14 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {{F}}^{-1}\left[{w}\right]\in \mathrm{Clsd}\left({J}\right)$
16 12 elin2d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {w}\in 𝒫{z}$
17 elpwi ${⊢}{w}\in 𝒫{z}\to {w}\subseteq {z}$
18 imass2 ${⊢}{w}\subseteq {z}\to {{F}}^{-1}\left[{w}\right]\subseteq {{F}}^{-1}\left[{z}\right]$
19 16 17 18 3syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to {{F}}^{-1}\left[{w}\right]\subseteq {{F}}^{-1}\left[{z}\right]$
20 nrmsep3 ${⊢}\left({J}\in \mathrm{Nrm}\wedge \left({{F}}^{-1}\left[{z}\right]\in {J}\wedge {{F}}^{-1}\left[{w}\right]\in \mathrm{Clsd}\left({J}\right)\wedge {{F}}^{-1}\left[{w}\right]\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)$
21 6 11 15 19 20 syl13anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)$
22 simplll ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
23 simprl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {u}\in {J}$
24 1 kqopn ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {u}\in {J}\right)\to {F}\left[{u}\right]\in \mathrm{KQ}\left({J}\right)$
25 22 23 24 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {F}\left[{u}\right]\in \mathrm{KQ}\left({J}\right)$
26 simprrl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {{F}}^{-1}\left[{w}\right]\subseteq {u}$
27 1 kqffn ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {F}Fn{X}$
28 fnfun ${⊢}{F}Fn{X}\to \mathrm{Fun}{F}$
29 22 27 28 3syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{Fun}{F}$
30 13 adantr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {w}\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)$
31 eqid ${⊢}\bigcup \mathrm{KQ}\left({J}\right)=\bigcup \mathrm{KQ}\left({J}\right)$
32 31 cldss ${⊢}{w}\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\to {w}\subseteq \bigcup \mathrm{KQ}\left({J}\right)$
33 30 32 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {w}\subseteq \bigcup \mathrm{KQ}\left({J}\right)$
34 toponuni ${⊢}\mathrm{KQ}\left({J}\right)\in \mathrm{TopOn}\left(\mathrm{ran}{F}\right)\to \mathrm{ran}{F}=\bigcup \mathrm{KQ}\left({J}\right)$
35 22 2 34 3syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{ran}{F}=\bigcup \mathrm{KQ}\left({J}\right)$
36 33 35 sseqtrrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {w}\subseteq \mathrm{ran}{F}$
37 funimass1 ${⊢}\left(\mathrm{Fun}{F}\wedge {w}\subseteq \mathrm{ran}{F}\right)\to \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\to {w}\subseteq {F}\left[{u}\right]\right)$
38 29 36 37 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\to {w}\subseteq {F}\left[{u}\right]\right)$
39 26 38 mpd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {w}\subseteq {F}\left[{u}\right]$
40 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
41 22 40 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {J}\in \mathrm{Top}$
42 elssuni ${⊢}{u}\in {J}\to {u}\subseteq \bigcup {J}$
43 42 ad2antrl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {u}\subseteq \bigcup {J}$
44 eqid ${⊢}\bigcup {J}=\bigcup {J}$
45 44 clscld ${⊢}\left({J}\in \mathrm{Top}\wedge {u}\subseteq \bigcup {J}\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\in \mathrm{Clsd}\left({J}\right)$
46 41 43 45 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\in \mathrm{Clsd}\left({J}\right)$
47 1 kqcld ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\in \mathrm{Clsd}\left({J}\right)\right)\to {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)$
48 22 46 47 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)$
49 44 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {u}\subseteq \bigcup {J}\right)\to {u}\subseteq \mathrm{cls}\left({J}\right)\left({u}\right)$
50 41 43 49 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {u}\subseteq \mathrm{cls}\left({J}\right)\left({u}\right)$
51 imass2 ${⊢}{u}\subseteq \mathrm{cls}\left({J}\right)\left({u}\right)\to {F}\left[{u}\right]\subseteq {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]$
52 50 51 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {F}\left[{u}\right]\subseteq {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]$
53 31 clsss2 ${⊢}\left({F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\in \mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\wedge {F}\left[{u}\right]\subseteq {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\right)\to \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]$
54 48 52 53 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]$
55 simprrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]$
56 44 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {u}\subseteq \bigcup {J}\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq \bigcup {J}$
57 41 43 56 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq \bigcup {J}$
58 fndm ${⊢}{F}Fn{X}\to \mathrm{dom}{F}={X}$
59 22 27 58 3syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{dom}{F}={X}$
60 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
61 22 60 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {X}=\bigcup {J}$
62 59 61 eqtrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{dom}{F}=\bigcup {J}$
63 57 62 sseqtrrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq \mathrm{dom}{F}$
64 funimass3 ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\subseteq {z}↔\mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)$
65 29 63 64 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \left({F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\subseteq {z}↔\mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)$
66 55 65 mpbird ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to {F}\left[\mathrm{cls}\left({J}\right)\left({u}\right)\right]\subseteq {z}$
67 54 66 sstrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {z}$
68 sseq2 ${⊢}{m}={F}\left[{u}\right]\to \left({w}\subseteq {m}↔{w}\subseteq {F}\left[{u}\right]\right)$
69 fveq2 ${⊢}{m}={F}\left[{u}\right]\to \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)=\mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)$
70 69 sseq1d ${⊢}{m}={F}\left[{u}\right]\to \left(\mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}↔\mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {z}\right)$
71 68 70 anbi12d ${⊢}{m}={F}\left[{u}\right]\to \left(\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)↔\left({w}\subseteq {F}\left[{u}\right]\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {z}\right)\right)$
72 71 rspcev ${⊢}\left({F}\left[{u}\right]\in \mathrm{KQ}\left({J}\right)\wedge \left({w}\subseteq {F}\left[{u}\right]\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({F}\left[{u}\right]\right)\subseteq {z}\right)\right)\to \exists {m}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)$
73 25 39 67 72 syl12anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\wedge \left({u}\in {J}\wedge \left({{F}}^{-1}\left[{w}\right]\subseteq {u}\wedge \mathrm{cls}\left({J}\right)\left({u}\right)\subseteq {{F}}^{-1}\left[{z}\right]\right)\right)\right)\to \exists {m}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)$
74 21 73 rexlimddv ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\wedge \left({z}\in \mathrm{KQ}\left({J}\right)\wedge {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\right)\right)\to \exists {m}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)$
75 74 ralrimivva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\to \forall {z}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)$
76 isnrm ${⊢}\mathrm{KQ}\left({J}\right)\in \mathrm{Nrm}↔\left(\mathrm{KQ}\left({J}\right)\in \mathrm{Top}\wedge \forall {z}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(\mathrm{Clsd}\left(\mathrm{KQ}\left({J}\right)\right)\cap 𝒫{z}\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in \mathrm{KQ}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({w}\subseteq {m}\wedge \mathrm{cls}\left(\mathrm{KQ}\left({J}\right)\right)\left({m}\right)\subseteq {z}\right)\right)$
77 5 75 76 sylanbrc ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Nrm}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{Nrm}$