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 )