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 ) |