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

Metamath Proof Explorer

Theorem kqreglem2

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

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

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) → 𝐽 ∈ Top )
4 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ( KQ ‘ 𝐽 ) ∈ Reg )
5 simpll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐽 )
7 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) )
9 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → 𝑤 ∈ 𝑧 )
10 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ⊆ 𝑋 )
11 5 6 10 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → 𝑧 ⊆ 𝑋 )
12 11 9 sseldd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → 𝑤 ∈ 𝑋 )
13 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) ) )
14 5 6 12 13 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ( 𝑤 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) ) )
15 9 14 mpbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) )
16 regsep ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Reg ∧ ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) ) → ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) )
17 4 8 15 16 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ∃ 𝑛 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) )
18 5 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 1 kqid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
20 18 19 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
21 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑛 ∈ ( KQ ‘ 𝐽 ) )
22 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ 𝑛 ∈ ( KQ ‘ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑛 ) ∈ 𝐽 )
23 20 21 22 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑛 ) ∈ 𝐽 )
24 12 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ∈ 𝑋 )
25 simprrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 )
26 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
27 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ) ) )
28 18 26 27 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ) ) )
29 24 25 28 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) )
30 1 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
31 topontop ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( KQ ‘ 𝐽 ) ∈ Top )
32 18 30 31 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( KQ ‘ 𝐽 ) ∈ Top )
33 elssuni ⊢ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) → 𝑛 ⊆ ∪ ( KQ ‘ 𝐽 ) )
34 33 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑛 ⊆ ∪ ( KQ ‘ 𝐽 ) )
35 eqid ⊢ ∪ ( KQ ‘ 𝐽 ) = ∪ ( KQ ‘ 𝐽 )
36 35 clscld ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑛 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
37 32 34 36 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
38 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ∈ ( Clsd ‘ 𝐽 ) )
39 20 37 38 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ∈ ( Clsd ‘ 𝐽 ) )
40 35 sscls ⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑛 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → 𝑛 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) )
41 32 34 40 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑛 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) )
42 imass2 ⊢ ( 𝑛 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) → ( ◡ 𝐹 “ 𝑛 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) )
43 41 42 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑛 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) )
44 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
45 44 clsss2 ⊢ ( ( ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ 𝐹 “ 𝑛 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) )
46 39 43 45 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) )
47 simprrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) )
48 imass2 ⊢ ( ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) )
49 47 48 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) )
50 6 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐽 )
51 1 kqsat ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 )
52 18 50 51 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 )
53 49 52 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ) ⊆ 𝑧 )
54 46 53 sstrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ 𝑧 )
55 eleq2 ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑛 ) → ( 𝑤 ∈ 𝑚 ↔ 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) ) )
56 fveq2 ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑛 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) = ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) )
57 56 sseq1d ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑛 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ↔ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ 𝑧 ) )
58 55 57 anbi12d ⊢ ( 𝑚 = ( ◡ 𝐹 “ 𝑛 ) → ( ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) ↔ ( 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ 𝑧 ) ) )
59 58 rspcev ⊢ ( ( ( ◡ 𝐹 “ 𝑛 ) ∈ 𝐽 ∧ ( 𝑤 ∈ ( ◡ 𝐹 “ 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑛 ) ) ⊆ 𝑧 ) ) → ∃ 𝑚 ∈ 𝐽 ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) )
60 23 29 54 59 syl12anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) ∧ ( 𝑛 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑛 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑛 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ∃ 𝑚 ∈ 𝐽 ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) )
61 17 60 rexlimddv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧 ) ) → ∃ 𝑚 ∈ 𝐽 ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) )
62 61 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) → ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ 𝑧 ∃ 𝑚 ∈ 𝐽 ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) )
63 isreg ⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ 𝑧 ∃ 𝑚 ∈ 𝐽 ( 𝑤 ∈ 𝑚 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑚 ) ⊆ 𝑧 ) ) )
64 3 62 63 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) → 𝐽 ∈ Reg )