Metamath Proof Explorer

Theorem txcnpi

Description: Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses txcnpi.1 
|- ( ph -> J e. ( TopOn ` X ) )
txcnpi.2 
|- ( ph -> K e. ( TopOn ` Y ) )
txcnpi.3 
|- ( ph -> F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) )
txcnpi.4 
|- ( ph -> U e. L )
txcnpi.5 
|- ( ph -> A e. X )
txcnpi.6 
|- ( ph -> B e. Y )
txcnpi.7 
|- ( ph -> ( A F B ) e. U )
Assertion txcnpi 
|- ( ph -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) )

Proof

Step Hyp Ref Expression
1 txcnpi.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 txcnpi.2 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 txcnpi.3 
 |-  ( ph -> F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) )
4 txcnpi.4 
 |-  ( ph -> U e. L )
5 txcnpi.5 
 |-  ( ph -> A e. X )
6 txcnpi.6 
 |-  ( ph -> B e. Y )
7 txcnpi.7 
 |-  ( ph -> ( A F B ) e. U )
8 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
9 8 7 eqeltrrid 
 |-  ( ph -> ( F ` <. A , B >. ) e. U )
10 cnpimaex 
 |-  ( ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) /\ U e. L /\ ( F ` <. A , B >. ) e. U ) -> E. w e. ( J tX K ) ( <. A , B >. e. w /\ ( F " w ) C_ U ) )
11 3 4 9 10 syl3anc 
 |-  ( ph -> E. w e. ( J tX K ) ( <. A , B >. e. w /\ ( F " w ) C_ U ) )
12 eqid 
 |-  U. ( J tX K ) = U. ( J tX K )
13 eqid 
 |-  U. L = U. L
14 12 13 cnpf 
 |-  ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) -> F : U. ( J tX K ) --> U. L )
15 3 14 syl 
 |-  ( ph -> F : U. ( J tX K ) --> U. L )
16 15 adantr 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> F : U. ( J tX K ) --> U. L )
17 16 ffund 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> Fun F )
18 elssuni 
 |-  ( w e. ( J tX K ) -> w C_ U. ( J tX K ) )
19 15 fdmd 
 |-  ( ph -> dom F = U. ( J tX K ) )
20 19 sseq2d 
 |-  ( ph -> ( w C_ dom F <-> w C_ U. ( J tX K ) ) )
21 20 biimpar 
 |-  ( ( ph /\ w C_ U. ( J tX K ) ) -> w C_ dom F )
22 18 21 sylan2 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> w C_ dom F )
23 funimass3 
 |-  ( ( Fun F /\ w C_ dom F ) -> ( ( F " w ) C_ U <-> w C_ ( `' F " U ) ) )
24 17 22 23 syl2anc 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( ( F " w ) C_ U <-> w C_ ( `' F " U ) ) )
25 24 anbi2d 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( ( <. A , B >. e. w /\ ( F " w ) C_ U ) <-> ( <. A , B >. e. w /\ w C_ ( `' F " U ) ) ) )
26 eltx 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( w e. ( J tX K ) <-> A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
27 1 2 26 syl2anc 
 |-  ( ph -> ( w e. ( J tX K ) <-> A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
28 27 biimpa 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) )
29 eleq1 
 |-  ( z = <. A , B >. -> ( z e. ( u X. v ) <-> <. A , B >. e. ( u X. v ) ) )
30 29 anbi1d 
 |-  ( z = <. A , B >. -> ( ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) <-> ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
31 30 2rexbidv 
 |-  ( z = <. A , B >. -> ( E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) <-> E. u e. J E. v e. K ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
32 31 rspccv 
 |-  ( A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( <. A , B >. e. w -> E. u e. J E. v e. K ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
33 sstr2 
 |-  ( ( u X. v ) C_ w -> ( w C_ ( `' F " U ) -> ( u X. v ) C_ ( `' F " U ) ) )
34 33 com12 
 |-  ( w C_ ( `' F " U ) -> ( ( u X. v ) C_ w -> ( u X. v ) C_ ( `' F " U ) ) )
35 34 anim2d 
 |-  ( w C_ ( `' F " U ) -> ( ( ( A e. u /\ B e. v ) /\ ( u X. v ) C_ w ) -> ( ( A e. u /\ B e. v ) /\ ( u X. v ) C_ ( `' F " U ) ) ) )
36 opelxp 
 |-  ( <. A , B >. e. ( u X. v ) <-> ( A e. u /\ B e. v ) )
37 36 anbi1i 
 |-  ( ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) <-> ( ( A e. u /\ B e. v ) /\ ( u X. v ) C_ w ) )
38 df-3an 
 |-  ( ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) <-> ( ( A e. u /\ B e. v ) /\ ( u X. v ) C_ ( `' F " U ) ) )
39 35 37 38 3imtr4g 
 |-  ( w C_ ( `' F " U ) -> ( ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
40 39 reximdv 
 |-  ( w C_ ( `' F " U ) -> ( E. v e. K ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
41 40 reximdv 
 |-  ( w C_ ( `' F " U ) -> ( E. u e. J E. v e. K ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
42 41 com12 
 |-  ( E. u e. J E. v e. K ( <. A , B >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( w C_ ( `' F " U ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
43 32 42 syl6 
 |-  ( A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( <. A , B >. e. w -> ( w C_ ( `' F " U ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) ) )
44 43 impd 
 |-  ( A. z e. w E. u e. J E. v e. K ( z e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( ( <. A , B >. e. w /\ w C_ ( `' F " U ) ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
45 28 44 syl 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( ( <. A , B >. e. w /\ w C_ ( `' F " U ) ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
46 25 45 sylbid 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( ( <. A , B >. e. w /\ ( F " w ) C_ U ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
47 46 rexlimdva 
 |-  ( ph -> ( E. w e. ( J tX K ) ( <. A , B >. e. w /\ ( F " w ) C_ U ) -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) ) )
48 11 47 mpd 
 |-  ( ph -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) )