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