Step |
Hyp |
Ref |
Expression |
1 |
|
cnnei.x |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
cnnei.y |
⊢ 𝑌 = ∪ 𝐾 |
3 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
4 |
2
|
toptopon |
⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
5 |
3 4
|
anbi12i |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ↔ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ) |
6 |
|
cncnp |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) ) ) |
7 |
6
|
baibd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) ) |
8 |
5 7
|
sylanb |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) ) |
9 |
5
|
anbi1i |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ↔ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
10 |
|
iscnp4 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) ) |
11 |
10
|
3expa |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) ) |
12 |
11
|
baibd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |
13 |
12
|
an32s |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |
14 |
9 13
|
sylanb |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |
15 |
14
|
ralbidva |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |
16 |
8 15
|
bitrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |
17 |
16
|
3impa |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) |