Step |
Hyp |
Ref |
Expression |
1 |
|
kqval.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) |
2 |
1
|
kqffn |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 ) |
3 |
2
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → 𝐹 Fn 𝑋 ) |
4 |
|
fncnvima2 |
⊢ ( 𝐹 Fn 𝑋 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) = { 𝑧 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑧 ) ∈ { ( 𝐹 ‘ 𝐴 ) } } ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) = { 𝑧 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑧 ) ∈ { ( 𝐹 ‘ 𝐴 ) } } ) |
6 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑧 ) ∈ V |
7 |
6
|
elsn |
⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ { ( 𝐹 ‘ 𝐴 ) } ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ) |
8 |
|
simpl1 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
9 |
|
simpr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 ) |
10 |
|
simpl3 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
11 |
1
|
kqfeq |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ) ) |
12 |
|
eleq2w |
⊢ ( 𝑦 = 𝑜 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑜 ) ) |
13 |
|
eleq2w |
⊢ ( 𝑦 = 𝑜 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑜 ) ) |
14 |
12 13
|
bibi12d |
⊢ ( 𝑦 = 𝑜 → ( ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) ) ) |
15 |
14
|
cbvralvw |
⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) ) |
16 |
11 15
|
bitrdi |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) ) ) |
17 |
8 9 10 16
|
syl3anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) ) ) |
18 |
7 17
|
syl5bb |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { ( 𝐹 ‘ 𝐴 ) } ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) ) ) |
19 |
18
|
rabbidva |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑧 ) ∈ { ( 𝐹 ‘ 𝐴 ) } } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) } ) |
20 |
5 19
|
eqtrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) } ) |
21 |
1
|
kqid |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |
22 |
21
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |
23 |
|
simp2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ Fre ) |
24 |
|
simp3 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
25 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) |
26 |
3 24 25
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) |
27 |
1
|
kqtopon |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) ) |
28 |
27
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) ) |
29 |
|
toponuni |
⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ran 𝐹 = ∪ ( KQ ‘ 𝐽 ) ) |
30 |
28 29
|
syl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 = ∪ ( KQ ‘ 𝐽 ) ) |
31 |
26 30
|
eleqtrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ∪ ( KQ ‘ 𝐽 ) ) |
32 |
|
eqid |
⊢ ∪ ( KQ ‘ 𝐽 ) = ∪ ( KQ ‘ 𝐽 ) |
33 |
32
|
t1sncld |
⊢ ( ( ( KQ ‘ 𝐽 ) ∈ Fre ∧ ( 𝐹 ‘ 𝐴 ) ∈ ∪ ( KQ ‘ 𝐽 ) ) → { ( 𝐹 ‘ 𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
34 |
23 31 33
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → { ( 𝐹 ‘ 𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) |
35 |
|
cnclima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ∧ { ( 𝐹 ‘ 𝐴 ) } ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ∈ ( Clsd ‘ 𝐽 ) ) |
36 |
22 34 35
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ∈ ( Clsd ‘ 𝐽 ) ) |
37 |
20 36
|
eqeltrrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑜 ∈ 𝐽 ( 𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) } ∈ ( Clsd ‘ 𝐽 ) ) |