Metamath Proof Explorer

Theorem ellimc2

Description: Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limccl.f 
|- ( ph -> F : A --> CC )
limccl.a 
|- ( ph -> A C_ CC )
limccl.b 
|- ( ph -> B e. CC )
ellimc2.k 
|- K = ( TopOpen ` CCfld )
Assertion ellimc2 
|- ( ph -> ( C e. ( F limCC B ) <-> ( C e. CC /\ A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )

Proof

Step Hyp Ref Expression
1 limccl.f 
 |-  ( ph -> F : A --> CC )
2 limccl.a 
 |-  ( ph -> A C_ CC )
3 limccl.b 
 |-  ( ph -> B e. CC )
4 ellimc2.k 
 |-  K = ( TopOpen ` CCfld )
5 limccl 
 |-  ( F limCC B ) C_ CC
6 5 sseli 
 |-  ( C e. ( F limCC B ) -> C e. CC )
7 6 pm4.71ri 
 |-  ( C e. ( F limCC B ) <-> ( C e. CC /\ C e. ( F limCC B ) ) )
8 eqid 
 |-  ( K |`t ( A u. { B } ) ) = ( K |`t ( A u. { B } ) )
9 eqid 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )
10 8 4 9 1 2 3 ellimc 
 |-  ( ph -> ( C e. ( F limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
11 10 adantr 
 |-  ( ( ph /\ C e. CC ) -> ( C e. ( F limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
12 4 cnfldtopon 
 |-  K e. ( TopOn ` CC )
13 3 snssd 
 |-  ( ph -> { B } C_ CC )
14 2 13 unssd 
 |-  ( ph -> ( A u. { B } ) C_ CC )
15 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
16 12 14 15 sylancr 
 |-  ( ph -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
17 16 adantr 
 |-  ( ( ph /\ C e. CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
18 12 a1i 
 |-  ( ( ph /\ C e. CC ) -> K e. ( TopOn ` CC ) )
19 ssun2 
 |-  { B } C_ ( A u. { B } )
20 snssg 
 |-  ( B e. CC -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
21 3 20 syl 
 |-  ( ph -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
22 19 21 mpbiri 
 |-  ( ph -> B e. ( A u. { B } ) )
23 22 adantr 
 |-  ( ( ph /\ C e. CC ) -> B e. ( A u. { B } ) )
24 elun 
 |-  ( z e. ( A u. { B } ) <-> ( z e. A \/ z e. { B } ) )
25 velsn 
 |-  ( z e. { B } <-> z = B )
26 25 orbi2i 
 |-  ( ( z e. A \/ z e. { B } ) <-> ( z e. A \/ z = B ) )
27 24 26 bitri 
 |-  ( z e. ( A u. { B } ) <-> ( z e. A \/ z = B ) )
28 simpllr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( z e. A \/ z = B ) ) /\ z = B ) -> C e. CC )
29 pm5.61 
 |-  ( ( ( z e. A \/ z = B ) /\ -. z = B ) <-> ( z e. A /\ -. z = B ) )
30 1 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
31 30 ad2ant2r 
 |-  ( ( ( ph /\ C e. CC ) /\ ( z e. A /\ -. z = B ) ) -> ( F ` z ) e. CC )
32 29 31 sylan2b 
 |-  ( ( ( ph /\ C e. CC ) /\ ( ( z e. A \/ z = B ) /\ -. z = B ) ) -> ( F ` z ) e. CC )
33 32 anassrs 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( z e. A \/ z = B ) ) /\ -. z = B ) -> ( F ` z ) e. CC )
34 28 33 ifclda 
 |-  ( ( ( ph /\ C e. CC ) /\ ( z e. A \/ z = B ) ) -> if ( z = B , C , ( F ` z ) ) e. CC )
35 27 34 sylan2b 
 |-  ( ( ( ph /\ C e. CC ) /\ z e. ( A u. { B } ) ) -> if ( z = B , C , ( F ` z ) ) e. CC )
36 35 fmpttd 
 |-  ( ( ph /\ C e. CC ) -> ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) : ( A u. { B } ) --> CC )
37 iscnp 
 |-  ( ( ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) /\ K e. ( TopOn ` CC ) /\ B e. ( A u. { B } ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) : ( A u. { B } ) --> CC /\ A. u e. K ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) ) ) )
38 37 baibd 
 |-  ( ( ( ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) /\ K e. ( TopOn ` CC ) /\ B e. ( A u. { B } ) ) /\ ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) : ( A u. { B } ) --> CC ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) <-> A. u e. K ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) ) )
39 17 18 23 36 38 syl31anc 
 |-  ( ( ph /\ C e. CC ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) <-> A. u e. K ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) ) )
40 iftrue 
 |-  ( z = B -> if ( z = B , C , ( F ` z ) ) = C )
41 40 9 fvmptg 
 |-  ( ( B e. ( A u. { B } ) /\ C e. CC ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) = C )
42 22 41 sylan 
 |-  ( ( ph /\ C e. CC ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) = C )
43 42 eleq1d 
 |-  ( ( ph /\ C e. CC ) -> ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u <-> C e. u ) )
44 43 imbi1d 
 |-  ( ( ph /\ C e. CC ) -> ( ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) <-> ( C e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) ) )
45 44 adantr 
 |-  ( ( ( ph /\ C e. CC ) /\ u e. K ) -> ( ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) <-> ( C e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) ) )
46 4 cnfldtop 
 |-  K e. Top
47 cnex 
 |-  CC e. _V
48 47 ssex 
 |-  ( ( A u. { B } ) C_ CC -> ( A u. { B } ) e. _V )
49 14 48 syl 
 |-  ( ph -> ( A u. { B } ) e. _V )
50 49 ad2antrr 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( A u. { B } ) e. _V )
51 restval 
 |-  ( ( K e. Top /\ ( A u. { B } ) e. _V ) -> ( K |`t ( A u. { B } ) ) = ran ( w e. K |-> ( w i^i ( A u. { B } ) ) ) )
52 46 50 51 sylancr 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( K |`t ( A u. { B } ) ) = ran ( w e. K |-> ( w i^i ( A u. { B } ) ) ) )
53 52 rexeqdv 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> E. v e. ran ( w e. K |-> ( w i^i ( A u. { B } ) ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) )
54 vex 
 |-  w e. _V
55 54 inex1 
 |-  ( w i^i ( A u. { B } ) ) e. _V
56 55 rgenw 
 |-  A. w e. K ( w i^i ( A u. { B } ) ) e. _V
57 eqid 
 |-  ( w e. K |-> ( w i^i ( A u. { B } ) ) ) = ( w e. K |-> ( w i^i ( A u. { B } ) ) )
58 eleq2 
 |-  ( v = ( w i^i ( A u. { B } ) ) -> ( B e. v <-> B e. ( w i^i ( A u. { B } ) ) ) )
59 imaeq2 
 |-  ( v = ( w i^i ( A u. { B } ) ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) = ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) )
60 59 sseq1d 
 |-  ( v = ( w i^i ( A u. { B } ) ) -> ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u <-> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) )
61 58 60 anbi12d 
 |-  ( v = ( w i^i ( A u. { B } ) ) -> ( ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> ( B e. ( w i^i ( A u. { B } ) ) /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) ) )
62 57 61 rexrnmptw 
 |-  ( A. w e. K ( w i^i ( A u. { B } ) ) e. _V -> ( E. v e. ran ( w e. K |-> ( w i^i ( A u. { B } ) ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> E. w e. K ( B e. ( w i^i ( A u. { B } ) ) /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) ) )
63 56 62 mp1i 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( E. v e. ran ( w e. K |-> ( w i^i ( A u. { B } ) ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> E. w e. K ( B e. ( w i^i ( A u. { B } ) ) /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) ) )
64 22 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> B e. ( A u. { B } ) )
65 elin 
 |-  ( B e. ( w i^i ( A u. { B } ) ) <-> ( B e. w /\ B e. ( A u. { B } ) ) )
66 65 rbaib 
 |-  ( B e. ( A u. { B } ) -> ( B e. ( w i^i ( A u. { B } ) ) <-> B e. w ) )
67 64 66 syl 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( B e. ( w i^i ( A u. { B } ) ) <-> B e. w ) )
68 simpllr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> C e. CC )
69 fvex 
 |-  ( F ` z ) e. _V
70 ifexg 
 |-  ( ( C e. CC /\ ( F ` z ) e. _V ) -> if ( z = B , C , ( F ` z ) ) e. _V )
71 68 69 70 sylancl 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> if ( z = B , C , ( F ` z ) ) e. _V )
72 71 ralrimivw 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. _V )
73 eqid 
 |-  ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) = ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) )
74 73 fnmpt 
 |-  ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. _V -> ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) Fn ( w i^i ( A u. { B } ) ) )
75 73 fmpt 
 |-  ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) : ( w i^i ( A u. { B } ) ) --> u )
76 df-f 
 |-  ( ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) : ( w i^i ( A u. { B } ) ) --> u <-> ( ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) Fn ( w i^i ( A u. { B } ) ) /\ ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u ) )
77 75 76 bitri 
 |-  ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ( ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) Fn ( w i^i ( A u. { B } ) ) /\ ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u ) )
78 77 baib 
 |-  ( ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) Fn ( w i^i ( A u. { B } ) ) -> ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u ) )
79 72 74 78 3syl 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u ) )
80 simplrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> C e. u )
81 elinel2 
 |-  ( z e. ( w i^i { B } ) -> z e. { B } )
82 25 40 sylbi 
 |-  ( z e. { B } -> if ( z = B , C , ( F ` z ) ) = C )
83 82 eleq1d 
 |-  ( z e. { B } -> ( if ( z = B , C , ( F ` z ) ) e. u <-> C e. u ) )
84 81 83 syl 
 |-  ( z e. ( w i^i { B } ) -> ( if ( z = B , C , ( F ` z ) ) e. u <-> C e. u ) )
85 80 84 syl5ibrcom 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( z e. ( w i^i { B } ) -> if ( z = B , C , ( F ` z ) ) e. u ) )
86 85 ralrimiv 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> A. z e. ( w i^i { B } ) if ( z = B , C , ( F ` z ) ) e. u )
87 undif1 
 |-  ( ( A \ { B } ) u. { B } ) = ( A u. { B } )
88 87 ineq2i 
 |-  ( w i^i ( ( A \ { B } ) u. { B } ) ) = ( w i^i ( A u. { B } ) )
89 indi 
 |-  ( w i^i ( ( A \ { B } ) u. { B } ) ) = ( ( w i^i ( A \ { B } ) ) u. ( w i^i { B } ) )
90 88 89 eqtr3i 
 |-  ( w i^i ( A u. { B } ) ) = ( ( w i^i ( A \ { B } ) ) u. ( w i^i { B } ) )
91 90 raleqi 
 |-  ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> A. z e. ( ( w i^i ( A \ { B } ) ) u. ( w i^i { B } ) ) if ( z = B , C , ( F ` z ) ) e. u )
92 ralunb 
 |-  ( A. z e. ( ( w i^i ( A \ { B } ) ) u. ( w i^i { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ( A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u /\ A. z e. ( w i^i { B } ) if ( z = B , C , ( F ` z ) ) e. u ) )
93 91 92 bitri 
 |-  ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> ( A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u /\ A. z e. ( w i^i { B } ) if ( z = B , C , ( F ` z ) ) e. u ) )
94 93 rbaib 
 |-  ( A. z e. ( w i^i { B } ) if ( z = B , C , ( F ` z ) ) e. u -> ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u ) )
95 86 94 syl 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( A. z e. ( w i^i ( A u. { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u ) )
96 79 95 bitr3d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u <-> A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u ) )
97 elinel2 
 |-  ( z e. ( w i^i ( A \ { B } ) ) -> z e. ( A \ { B } ) )
98 eldifsni 
 |-  ( z e. ( A \ { B } ) -> z =/= B )
99 ifnefalse 
 |-  ( z =/= B -> if ( z = B , C , ( F ` z ) ) = ( F ` z ) )
100 98 99 syl 
 |-  ( z e. ( A \ { B } ) -> if ( z = B , C , ( F ` z ) ) = ( F ` z ) )
101 100 eleq1d 
 |-  ( z e. ( A \ { B } ) -> ( if ( z = B , C , ( F ` z ) ) e. u <-> ( F ` z ) e. u ) )
102 97 101 syl 
 |-  ( z e. ( w i^i ( A \ { B } ) ) -> ( if ( z = B , C , ( F ` z ) ) e. u <-> ( F ` z ) e. u ) )
103 102 ralbiia 
 |-  ( A. z e. ( w i^i ( A \ { B } ) ) if ( z = B , C , ( F ` z ) ) e. u <-> A. z e. ( w i^i ( A \ { B } ) ) ( F ` z ) e. u )
104 96 103 bitrdi 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u <-> A. z e. ( w i^i ( A \ { B } ) ) ( F ` z ) e. u ) )
105 df-ima 
 |-  ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) = ran ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) |` ( w i^i ( A u. { B } ) ) )
106 inss2 
 |-  ( w i^i ( A u. { B } ) ) C_ ( A u. { B } )
107 resmpt 
 |-  ( ( w i^i ( A u. { B } ) ) C_ ( A u. { B } ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) |` ( w i^i ( A u. { B } ) ) ) = ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) )
108 106 107 mp1i 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) |` ( w i^i ( A u. { B } ) ) ) = ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) )
109 108 rneqd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ran ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) |` ( w i^i ( A u. { B } ) ) ) = ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) )
110 105 109 eqtrid 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) = ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) )
111 110 sseq1d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u <-> ran ( z e. ( w i^i ( A u. { B } ) ) |-> if ( z = B , C , ( F ` z ) ) ) C_ u ) )
112 1 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> F : A --> CC )
113 112 ffund 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> Fun F )
114 inss2 
 |-  ( w i^i ( A \ { B } ) ) C_ ( A \ { B } )
115 difss 
 |-  ( A \ { B } ) C_ A
116 114 115 sstri 
 |-  ( w i^i ( A \ { B } ) ) C_ A
117 112 fdmd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> dom F = A )
118 116 117 sseqtrrid 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( w i^i ( A \ { B } ) ) C_ dom F )
119 funimass4 
 |-  ( ( Fun F /\ ( w i^i ( A \ { B } ) ) C_ dom F ) -> ( ( F " ( w i^i ( A \ { B } ) ) ) C_ u <-> A. z e. ( w i^i ( A \ { B } ) ) ( F ` z ) e. u ) )
120 113 118 119 syl2anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( F " ( w i^i ( A \ { B } ) ) ) C_ u <-> A. z e. ( w i^i ( A \ { B } ) ) ( F ` z ) e. u ) )
121 104 111 120 3bitr4d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u <-> ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) )
122 67 121 anbi12d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) /\ w e. K ) -> ( ( B e. ( w i^i ( A u. { B } ) ) /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) <-> ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) )
123 122 rexbidva 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( E. w e. K ( B e. ( w i^i ( A u. { B } ) ) /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " ( w i^i ( A u. { B } ) ) ) C_ u ) <-> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) )
124 53 63 123 3bitrd 
 |-  ( ( ( ph /\ C e. CC ) /\ ( u e. K /\ C e. u ) ) -> ( E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) )
125 124 anassrs 
 |-  ( ( ( ( ph /\ C e. CC ) /\ u e. K ) /\ C e. u ) -> ( E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) <-> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) )
126 125 pm5.74da 
 |-  ( ( ( ph /\ C e. CC ) /\ u e. K ) -> ( ( C e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) <-> ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) )
127 45 126 bitrd 
 |-  ( ( ( ph /\ C e. CC ) /\ u e. K ) -> ( ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) <-> ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) )
128 127 ralbidva 
 |-  ( ( ph /\ C e. CC ) -> ( A. u e. K ( ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) ` B ) e. u -> E. v e. ( K |`t ( A u. { B } ) ) ( B e. v /\ ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) " v ) C_ u ) ) <-> A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) )
129 11 39 128 3bitrd 
 |-  ( ( ph /\ C e. CC ) -> ( C e. ( F limCC B ) <-> A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) )
130 129 pm5.32da 
 |-  ( ph -> ( ( C e. CC /\ C e. ( F limCC B ) ) <-> ( C e. CC /\ A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
131 7 130 syl5bb 
 |-  ( ph -> ( C e. ( F limCC B ) <-> ( C e. CC /\ A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )