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

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 )