Metamath Proof Explorer

Theorem limcfval

Description: Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion limcfval ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )

Proof

Step Hyp Ref Expression
1 limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
2 limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 df-limc ⊢ limℂ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } )
4 3 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → limℂ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } ) )
5 fvexd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) → ( TopOpen ‘ ℂfld ) ∈ V )
6 simplrl ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → 𝑓 = 𝐹 )
7 6 dmeqd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → dom 𝑓 = dom 𝐹 )
8 simpll1 ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → 𝐹 : 𝐴 ⟶ ℂ )
9 8 fdmd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → dom 𝐹 = 𝐴 )
10 7 9 eqtrd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → dom 𝑓 = 𝐴 )
11 simplrr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → 𝑥 = 𝐵 )
12 11 sneqd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → { 𝑥 } = { 𝐵 } )
13 10 12 uneq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( dom 𝑓 ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝐵 } ) )
14 11 eqeq2d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝐵 ) )
15 6 fveq1d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
16 14 15 ifbieq2d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) )
17 13 16 mpteq12dv ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) )
18 simpr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → 𝑗 = ( TopOpen ‘ ℂfld ) )
19 18 2 eqtr4di ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → 𝑗 = 𝐾 )
20 19 13 oveq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) )
21 20 1 eqtr4di ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) = 𝐽 )
22 21 19 oveq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) = ( 𝐽 CnP 𝐾 ) )
23 22 11 fveq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) = ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
24 17 23 eleq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) ∧ 𝑗 = ( TopOpen ‘ ℂfld ) ) → ( ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
25 5 24 sbcied ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) → ( [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
26 25 abbidv ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝐵 ) ) → { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } )
27 cnex ⊢ ℂ ∈ V
28 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
29 27 27 28 mpanl12 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
30 29 3adant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
31 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
32 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) )
33 1 2 32 limcvallem ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝑦 ∈ ℂ ) )
34 33 abssdv ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ⊆ ℂ )
35 27 ssex ⊢ ( { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ⊆ ℂ → { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∈ V )
36 34 35 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∈ V )
37 4 26 30 31 36 ovmpod ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } )
38 37 34 eqsstrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 limℂ 𝐵 ) ⊆ ℂ )
39 37 38 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )