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