Step |
Hyp |
Ref |
Expression |
1 |
|
cnplimc.k |
⊢ 𝐾 = ( TopOpen ‘ ℂfld ) |
2 |
|
cnplimc.j |
⊢ 𝐽 = ( 𝐾 ↾t 𝐴 ) |
3 |
1
|
cnfldtopon |
⊢ 𝐾 ∈ ( TopOn ‘ ℂ ) |
4 |
|
simpl |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ⊆ ℂ ) |
5 |
|
resttopon |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( 𝐾 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ) |
6 |
3 4 5
|
sylancr |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐾 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ) |
7 |
2 6
|
eqeltrid |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) |
8 |
|
cnpf2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐹 : 𝐴 ⟶ ℂ ) |
9 |
8
|
3expia |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐹 : 𝐴 ⟶ ℂ ) ) |
10 |
7 3 9
|
sylancl |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐹 : 𝐴 ⟶ ℂ ) ) |
11 |
10
|
pm4.71rd |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) ) ) |
12 |
|
simpr |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ ) |
13 |
|
simplr |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐵 ∈ 𝐴 ) |
14 |
13
|
snssd |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → { 𝐵 } ⊆ 𝐴 ) |
15 |
|
ssequn2 |
⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝐵 } ) = 𝐴 ) |
16 |
14 15
|
sylib |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐴 ∪ { 𝐵 } ) = 𝐴 ) |
17 |
16
|
feq2d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ↔ 𝐹 : 𝐴 ⟶ ℂ ) ) |
18 |
12 17
|
mpbird |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ) |
19 |
18
|
feqmptd |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
20 |
16
|
oveq2d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t 𝐴 ) ) |
21 |
2 20
|
eqtr4id |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ) |
22 |
21
|
oveq1d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐽 CnP 𝐾 ) = ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ) |
23 |
22
|
fveq1d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) = ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) |
24 |
19 23
|
eleq12d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) ) |
25 |
|
eqid |
⊢ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) |
26 |
|
ifid |
⊢ if ( 𝑥 = 𝐵 , ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) |
27 |
|
fveq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) |
28 |
27
|
adantl |
⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) |
29 |
28
|
ifeq1da |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) → if ( 𝑥 = 𝐵 , ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ) = if ( 𝑥 = 𝐵 , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝑥 ) ) ) |
30 |
26 29
|
syl5eqr |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 𝐵 , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝑥 ) ) ) |
31 |
30
|
mpteq2ia |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝑥 ) ) ) |
32 |
|
simpll |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ⊆ ℂ ) |
33 |
32 13
|
sseldd |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐵 ∈ ℂ ) |
34 |
25 1 31 12 32 33
|
ellimc |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) ) |
35 |
24 34
|
bitr4d |
⊢ ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) |
36 |
35
|
pm5.32da |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) ) |
37 |
11 36
|
bitrd |
⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) ) |