Step |
Hyp |
Ref |
Expression |
1 |
|
cncnp |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ) |
2 |
|
simplr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
3 |
|
cnpfcf |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) ) |
4 |
3
|
ad4ant124 |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) ) |
5 |
2 4
|
mpbirand |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
6 |
5
|
ralbidva |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
7 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) |
8 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
9 |
8
|
fclselbas |
⊢ ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → 𝑥 ∈ ∪ 𝐽 ) |
10 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
11 |
10
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝑋 = ∪ 𝐽 ) |
12 |
11
|
eleq2d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽 ) ) |
13 |
9 12
|
syl5ibr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → 𝑥 ∈ 𝑋 ) ) |
14 |
13
|
pm4.71rd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) ) ) |
15 |
14
|
imbi1d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
16 |
|
impexp |
⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ 𝑋 → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
17 |
15 16
|
bitrdi |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ 𝑋 → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) ) |
18 |
17
|
ralbidv2 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
19 |
18
|
ralbidv |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
20 |
7 19
|
bitr4id |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) |
21 |
6 20
|
bitrd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) |
22 |
21
|
pm5.32da |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |
23 |
1 22
|
bitrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) |