Metamath Proof Explorer


Theorem kqreglem1

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

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

Proof

Step Hyp Ref Expression
1 kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
2 1 kqtopon ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
3 2 adantr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
4 topontop ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( KQ ‘ 𝐽 ) ∈ Top )
5 3 4 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Top )
6 toponss ( ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) → 𝑎 ⊆ ran 𝐹 )
7 3 6 sylan ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) → 𝑎 ⊆ ran 𝐹 )
8 7 sselda ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → 𝑏 ∈ ran 𝐹 )
9 1 kqffn ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
10 9 ad3antrrr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → 𝐹 Fn 𝑋 )
11 fvelrnb ( 𝐹 Fn 𝑋 → ( 𝑏 ∈ ran 𝐹 ↔ ∃ 𝑧𝑋 ( 𝐹𝑧 ) = 𝑏 ) )
12 10 11 syl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → ( 𝑏 ∈ ran 𝐹 ↔ ∃ 𝑧𝑋 ( 𝐹𝑧 ) = 𝑏 ) )
13 8 12 mpbid ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → ∃ 𝑧𝑋 ( 𝐹𝑧 ) = 𝑏 )
14 simpllr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → 𝐽 ∈ Reg )
15 1 kqid ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
16 15 ad3antrrr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) )
17 simplr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → 𝑎 ∈ ( KQ ‘ 𝐽 ) )
18 cnima ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) → ( 𝐹𝑎 ) ∈ 𝐽 )
19 16 17 18 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → ( 𝐹𝑎 ) ∈ 𝐽 )
20 9 adantr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → 𝐹 Fn 𝑋 )
21 20 adantr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) → 𝐹 Fn 𝑋 )
22 elpreima ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( 𝐹𝑎 ) ↔ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) )
23 21 22 syl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) → ( 𝑧 ∈ ( 𝐹𝑎 ) ↔ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) )
24 23 biimpar ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → 𝑧 ∈ ( 𝐹𝑎 ) )
25 regsep ( ( 𝐽 ∈ Reg ∧ ( 𝐹𝑎 ) ∈ 𝐽𝑧 ∈ ( 𝐹𝑎 ) ) → ∃ 𝑤𝐽 ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) )
26 14 19 24 25 syl3anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → ∃ 𝑤𝐽 ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) )
27 simp-4l ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
28 simprl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝑤𝐽 )
29 1 kqopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤𝐽 ) → ( 𝐹𝑤 ) ∈ ( KQ ‘ 𝐽 ) )
30 27 28 29 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝐹𝑤 ) ∈ ( KQ ‘ 𝐽 ) )
31 simprrl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝑧𝑤 )
32 simplrl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝑧𝑋 )
33 1 kqfvima ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤𝐽𝑧𝑋 ) → ( 𝑧𝑤 ↔ ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) ) )
34 27 28 32 33 syl3anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝑧𝑤 ↔ ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) ) )
35 31 34 mpbid ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) )
36 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
37 27 36 syl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝐽 ∈ Top )
38 elssuni ( 𝑤𝐽𝑤 𝐽 )
39 38 ad2antrl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝑤 𝐽 )
40 eqid 𝐽 = 𝐽
41 40 clscld ( ( 𝐽 ∈ Top ∧ 𝑤 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ∈ ( Clsd ‘ 𝐽 ) )
42 37 39 41 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ∈ ( Clsd ‘ 𝐽 ) )
43 1 kqcld ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
44 27 42 43 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )
45 40 sscls ( ( 𝐽 ∈ Top ∧ 𝑤 𝐽 ) → 𝑤 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) )
46 37 39 45 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝑤 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) )
47 imass2 ( 𝑤 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) → ( 𝐹𝑤 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
48 46 47 syl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝐹𝑤 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
49 eqid ( KQ ‘ 𝐽 ) = ( KQ ‘ 𝐽 )
50 49 clsss2 ( ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ∧ ( 𝐹𝑤 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
51 44 48 50 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
52 20 ad3antrrr ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → 𝐹 Fn 𝑋 )
53 fnfun ( 𝐹 Fn 𝑋 → Fun 𝐹 )
54 52 53 syl ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → Fun 𝐹 )
55 simprrr ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) )
56 funimass2 ( ( Fun 𝐹 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ⊆ 𝑎 )
57 54 55 56 syl2anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ⊆ 𝑎 )
58 51 57 sstrd ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ 𝑎 )
59 eleq2 ( 𝑚 = ( 𝐹𝑤 ) → ( ( 𝐹𝑧 ) ∈ 𝑚 ↔ ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) ) )
60 fveq2 ( 𝑚 = ( 𝐹𝑤 ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) = ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) )
61 60 sseq1d ( 𝑚 = ( 𝐹𝑤 ) → ( ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ↔ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ 𝑎 ) )
62 59 61 anbi12d ( 𝑚 = ( 𝐹𝑤 ) → ( ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ↔ ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ 𝑎 ) ) )
63 62 rspcev ( ( ( 𝐹𝑤 ) ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹𝑧 ) ∈ ( 𝐹𝑤 ) ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ ( 𝐹𝑤 ) ) ⊆ 𝑎 ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
64 30 35 58 63 syl12anc ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) ∧ ( 𝑤𝐽 ∧ ( 𝑧𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝐹𝑎 ) ) ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
65 26 64 rexlimddv ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ ( 𝑧𝑋 ∧ ( 𝐹𝑧 ) ∈ 𝑎 ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
66 65 expr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑧𝑋 ) → ( ( 𝐹𝑧 ) ∈ 𝑎 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
67 eleq1 ( ( 𝐹𝑧 ) = 𝑏 → ( ( 𝐹𝑧 ) ∈ 𝑎𝑏𝑎 ) )
68 eleq1 ( ( 𝐹𝑧 ) = 𝑏 → ( ( 𝐹𝑧 ) ∈ 𝑚𝑏𝑚 ) )
69 68 anbi1d ( ( 𝐹𝑧 ) = 𝑏 → ( ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ↔ ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
70 69 rexbidv ( ( 𝐹𝑧 ) = 𝑏 → ( ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ↔ ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
71 67 70 imbi12d ( ( 𝐹𝑧 ) = 𝑏 → ( ( ( 𝐹𝑧 ) ∈ 𝑎 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹𝑧 ) ∈ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) ↔ ( 𝑏𝑎 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) ) )
72 66 71 syl5ibcom ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑧𝑋 ) → ( ( 𝐹𝑧 ) = 𝑏 → ( 𝑏𝑎 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) ) )
73 72 com23 ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑧𝑋 ) → ( 𝑏𝑎 → ( ( 𝐹𝑧 ) = 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) ) )
74 73 imp ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑧𝑋 ) ∧ 𝑏𝑎 ) → ( ( 𝐹𝑧 ) = 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
75 74 an32s ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) ∧ 𝑧𝑋 ) → ( ( 𝐹𝑧 ) = 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
76 75 rexlimdva ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → ( ∃ 𝑧𝑋 ( 𝐹𝑧 ) = 𝑏 → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
77 13 76 mpd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ 𝑎 ∈ ( KQ ‘ 𝐽 ) ) ∧ 𝑏𝑎 ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
78 77 anasss ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑎 ∈ ( KQ ‘ 𝐽 ) ∧ 𝑏𝑎 ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
79 78 ralrimivva ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ∀ 𝑎 ∈ ( KQ ‘ 𝐽 ) ∀ 𝑏𝑎𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) )
80 isreg ( ( KQ ‘ 𝐽 ) ∈ Reg ↔ ( ( KQ ‘ 𝐽 ) ∈ Top ∧ ∀ 𝑎 ∈ ( KQ ‘ 𝐽 ) ∀ 𝑏𝑎𝑚 ∈ ( KQ ‘ 𝐽 ) ( 𝑏𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ 𝑎 ) ) )
81 5 79 80 sylanbrc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Reg )