| Step |
Hyp |
Ref |
Expression |
| 1 |
|
kqval.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) |
| 2 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
| 3 |
2
|
adantr |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Top ) |
| 4 |
|
simplr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( KQ ‘ 𝐽 ) ∈ Nrm ) |
| 5 |
|
simpll |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
| 6 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑧 ∈ 𝐽 ) |
| 7 |
1
|
kqopn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ) |
| 8 |
5 6 7
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ) |
| 9 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) |
| 10 |
9
|
elin1d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( Clsd ‘ 𝐽 ) ) |
| 11 |
1
|
kqcld |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
| 12 |
5 10 11
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
| 13 |
9
|
elin2d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ 𝒫 𝑧 ) |
| 14 |
|
elpwi |
⊢ ( 𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧 ) |
| 15 |
|
imass2 |
⊢ ( 𝑤 ⊆ 𝑧 → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) ) |
| 16 |
13 14 15
|
3syl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) ) |
| 17 |
|
nrmsep3 |
⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Nrm ∧ ( ( 𝐹 “ 𝑧 ) ∈ ( KQ ‘ 𝐽 ) ∧ ( 𝐹 “ 𝑤 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ∧ ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) |
| 18 |
4 8 12 16 17
|
syl13anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ∃ 𝑚 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) |
| 19 |
|
simplll |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
| 20 |
1
|
kqid |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |
| 21 |
19 20
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |
| 22 |
|
simprl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ∈ ( KQ ‘ 𝐽 ) ) |
| 23 |
|
cnima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ 𝑚 ∈ ( KQ ‘ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 ) |
| 24 |
21 22 23
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 ) |
| 25 |
|
simprrl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ) |
| 26 |
1
|
kqffn |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 ) |
| 27 |
|
fnfun |
⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 ) |
| 28 |
19 26 27
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → Fun 𝐹 ) |
| 29 |
10
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ∈ ( Clsd ‘ 𝐽 ) ) |
| 30 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
| 31 |
30
|
cldss |
⊢ ( 𝑤 ∈ ( Clsd ‘ 𝐽 ) → 𝑤 ⊆ ∪ 𝐽 ) |
| 32 |
29 31
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ ∪ 𝐽 ) |
| 33 |
|
fndm |
⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 ) |
| 34 |
19 26 33
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → dom 𝐹 = 𝑋 ) |
| 35 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
| 36 |
19 35
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑋 = ∪ 𝐽 ) |
| 37 |
34 36
|
eqtrd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → dom 𝐹 = ∪ 𝐽 ) |
| 38 |
32 37
|
sseqtrrd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ dom 𝐹 ) |
| 39 |
|
funimass3 |
⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) ) |
| 40 |
28 38 39
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) ) |
| 41 |
25 40
|
mpbid |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) |
| 42 |
1
|
kqtopon |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) ) |
| 43 |
|
topontop |
⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( KQ ‘ 𝐽 ) ∈ Top ) |
| 44 |
19 42 43
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( KQ ‘ 𝐽 ) ∈ Top ) |
| 45 |
|
elssuni |
⊢ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) → 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) |
| 46 |
45
|
ad2antrl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) |
| 47 |
|
eqid |
⊢ ∪ ( KQ ‘ 𝐽 ) = ∪ ( KQ ‘ 𝐽 ) |
| 48 |
47
|
clscld |
⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
| 49 |
44 46 48
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
| 50 |
|
cnclima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
| 51 |
21 49 50
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
| 52 |
47
|
sscls |
⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Top ∧ 𝑚 ⊆ ∪ ( KQ ‘ 𝐽 ) ) → 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) |
| 53 |
44 46 52
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) |
| 54 |
|
imass2 |
⊢ ( 𝑚 ⊆ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) → ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) |
| 55 |
53 54
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) |
| 56 |
30
|
clsss2 |
⊢ ( ( ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ 𝐹 “ 𝑚 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) |
| 57 |
51 55 56
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ) |
| 58 |
|
simprrr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) |
| 59 |
|
imass2 |
⊢ ( ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) ) |
| 60 |
58 59
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) ) |
| 61 |
6
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐽 ) |
| 62 |
1
|
kqsat |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 ) |
| 63 |
19 61 62
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑧 ) ) = 𝑧 ) |
| 64 |
60 63
|
sseqtrd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ◡ 𝐹 “ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ) ⊆ 𝑧 ) |
| 65 |
57 64
|
sstrd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) |
| 66 |
|
sseq2 |
⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( 𝑤 ⊆ 𝑢 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ) ) |
| 67 |
|
fveq2 |
⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) = ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ) |
| 68 |
67
|
sseq1d |
⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ↔ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) ) |
| 69 |
66 68
|
anbi12d |
⊢ ( 𝑢 = ( ◡ 𝐹 “ 𝑚 ) → ( ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ↔ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) ) ) |
| 70 |
69
|
rspcev |
⊢ ( ( ( ◡ 𝐹 “ 𝑚 ) ∈ 𝐽 ∧ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑚 ) ) ⊆ 𝑧 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) |
| 71 |
24 41 65 70
|
syl12anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) ∧ ( 𝑚 ∈ ( KQ ‘ 𝐽 ) ∧ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑚 ∧ ( ( cls ‘ ( KQ ‘ 𝐽 ) ) ‘ 𝑚 ) ⊆ ( 𝐹 “ 𝑧 ) ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) |
| 72 |
18 71
|
rexlimddv |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) |
| 73 |
72
|
ralrimivva |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) |
| 74 |
|
isnrm |
⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝐽 ∀ 𝑤 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑧 ) ∃ 𝑢 ∈ 𝐽 ( 𝑤 ⊆ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑧 ) ) ) |
| 75 |
3 73 74
|
sylanbrc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Nrm ) → 𝐽 ∈ Nrm ) |