Step |
Hyp |
Ref |
Expression |
1 |
|
cnfdmsn |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) ∈ ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) ) |
2 |
|
snssi |
⊢ ( 𝐴 ∈ ℂ → { 𝐴 } ⊆ ℂ ) |
3 |
|
snssi |
⊢ ( 𝐵 ∈ ℂ → { 𝐵 } ⊆ ℂ ) |
4 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
5 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) = ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) |
6 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) = ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) |
7 |
4 5 6
|
cncfcn |
⊢ ( ( { 𝐴 } ⊆ ℂ ∧ { 𝐵 } ⊆ ℂ ) → ( { 𝐴 } –cn→ { 𝐵 } ) = ( ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) Cn ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) ) ) |
8 |
2 3 7
|
syl2an |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( { 𝐴 } –cn→ { 𝐵 } ) = ( ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) Cn ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) ) ) |
9 |
4
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
10 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ ) |
11 |
|
restsn2 |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) = 𝒫 { 𝐴 } ) |
12 |
9 10 11
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) = 𝒫 { 𝐴 } ) |
13 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ ) |
14 |
|
restsn2 |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐵 ∈ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) = 𝒫 { 𝐵 } ) |
15 |
9 13 14
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) = 𝒫 { 𝐵 } ) |
16 |
12 15
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( TopOpen ‘ ℂfld ) ↾t { 𝐴 } ) Cn ( ( TopOpen ‘ ℂfld ) ↾t { 𝐵 } ) ) = ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) ) |
17 |
8 16
|
eqtr2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) = ( { 𝐴 } –cn→ { 𝐵 } ) ) |
18 |
1 17
|
eleqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) ∈ ( { 𝐴 } –cn→ { 𝐵 } ) ) |