Step |
Hyp |
Ref |
Expression |
1 |
|
cncnp.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
cncnp.2 |
⊢ 𝑌 = ∪ 𝐾 |
3 |
|
cntop1 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top ) |
4 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
5 |
3 4
|
sylib |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
6 |
|
cntop2 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top ) |
7 |
2
|
toptopon |
⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
8 |
6 7
|
sylib |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
9 |
1 2
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
10 |
5 8 9
|
jca31 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
12 |
|
r19.2z |
⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) → ∃ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) |
13 |
|
cnptop1 |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐽 ∈ Top ) |
14 |
13 4
|
sylib |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
15 |
|
cnptop2 |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐾 ∈ Top ) |
16 |
15 7
|
sylib |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
17 |
1 2
|
cnpf |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
18 |
14 16 17
|
jca31 |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
19 |
18
|
rexlimivw |
⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
20 |
12 19
|
syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ) |
21 |
|
cncnp |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ) |
22 |
21
|
baibd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) |
23 |
11 20 22
|
pm5.21nd |
⊢ ( 𝑋 ≠ ∅ → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) |