Metamath Proof Explorer

Theorem iscnp3

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". (Contributed by NM, 15-May-2007)

Ref Expression
Assertion iscnp3 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
2 ffun 
 |-  ( F : X --> Y -> Fun F )
3 2 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> Fun F )
4 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
5 4 adantlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> x C_ X )
6 fdm 
 |-  ( F : X --> Y -> dom F = X )
7 6 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> dom F = X )
8 5 7 sseqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> x C_ dom F )
9 funimass3 
 |-  ( ( Fun F /\ x C_ dom F ) -> ( ( F " x ) C_ y <-> x C_ ( `' F " y ) ) )
10 3 8 9 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> ( ( F " x ) C_ y <-> x C_ ( `' F " y ) ) )
11 10 anbi2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) /\ x e. J ) -> ( ( P e. x /\ ( F " x ) C_ y ) <-> ( P e. x /\ x C_ ( `' F " y ) ) ) )
12 11 rexbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) <-> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) )
13 12 imbi2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) -> ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) )
14 13 ralbidv 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X --> Y ) -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) )
15 14 pm5.32da 
 |-  ( J e. ( TopOn ` X ) -> ( ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )
16 15 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )
17 1 16 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )