This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kqnrmlem2

Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion kqnrmlem2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Nrm )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Top )
4 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( KQ ‘ 𝐽 ) ∈ Nrm )
5 simpll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑧 ∈ 𝐽 )
7 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
9 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) )
10 9 elin1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( Clsd ‘ 𝐽 ) )
11 1 kqcld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
12 5 10 11 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
13 9 elin2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ 𝒫 𝑧 )
14 elpwi ⊢ ( 𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧 )
15 imass2 ⊢ ( 𝑤 ⊆ 𝑧 → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) )
16 13 14 15 3syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) )
17 nrmsep3 ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Nrm ∧ ( ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ∧ ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ∧ ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) )
18 4 8 12 16 17 syl13anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) )
19 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
20 1 kqid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
21 19 20 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
22 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ∈ ( KQ ‘ 𝐽 ) )
23 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ 𝑚 ∈ ( KQ ‘ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 )
24 21 22 23 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 )
25 simprrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑚 )
26 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
27 fnfun ⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
28 19 26 27 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → Fun 𝐹 )
29 10 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ∈ ( Clsd ‘ 𝐽 ) )
30 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
31 30 cldss ⊢ ( 𝑤 ∈ ( Clsd ‘ 𝐽 ) → 𝑤 ⊆ ∪ 𝐽 )
32 29 31 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ ∪ 𝐽 )
33 fndm ⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
34 19 26 33 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → dom 𝐹 = 𝑋 )
35 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
36 19 35 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑋 = ∪ 𝐽 )
37 34 36 eqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → dom 𝐹 = ∪ 𝐽 )
38 32 37 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ dom 𝐹 )
39 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) )
40 28 38 39 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) )
41 25 40 mpbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) )
42 1 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
43 topontop ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( KQ ‘ 𝐽 ) ∈ Top )
44 19 42 43 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( KQ ‘ 𝐽 ) ∈ Top )
45 elssuni ⊢ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) → 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) )
46 45 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) )
47 eqid ⊢ ∪ ( KQ ‘ 𝐽 ) = ∪ ( KQ ‘ 𝐽 )
48 47 clscld ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
49 44 46 48 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
50 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) )
51 21 49 50 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) )
52 47 sscls ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) )
53 44 46 52 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) )
54 imass2 ⊢ ( 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) → ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) )
55 53 54 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) )
56 30 clsss2 ⊢ ( ( ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) )
57 51 55 56 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) )
58 simprrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) )
59 imass2 ⊢ ( ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) )
60 58 59 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) )
61 6 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐽 )
62 1 kqsat ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 )
63 19 61 62 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 )
64 60 63 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ 𝑧 )
65 57 64 sstrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 )
66 sseq2 ⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( 𝑤 ⊆ 𝑢 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) )
67 fveq2 ⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) = ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) )
68 67 sseq1d ⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ↔ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) )
69 66 68 anbi12d ⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ↔ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) ) )
70 69 rspcev ⊢ ( ( ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 ∧ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) )
71 24 41 65 70 syl12anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) )
72 18 71 rexlimddv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) )
73 72 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) )
74 isnrm ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) )
75 3 73 74 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Nrm )