Metamath Proof Explorer

Theorem cnpflfi

Description: Forward direction of cnpflf . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnpflfi 
|- ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fLimf L ) ` F ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 cnpf 
 |-  ( F e. ( ( J CnP K ) ` A ) -> F : U. J --> U. K )
4 3 adantl 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : U. J --> U. K )
5 1 flimelbas 
 |-  ( A e. ( J fLim L ) -> A e. U. J )
6 5 adantr 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> A e. U. J )
7 4 6 ffvelcdmd 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. U. K )
8 simplr 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> F e. ( ( J CnP K ) ` A ) )
9 simprl 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> x e. K )
10 simprr 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> ( F ` A ) e. x )
11 cnpimaex 
 |-  ( ( F e. ( ( J CnP K ) ` A ) /\ x e. K /\ ( F ` A ) e. x ) -> E. y e. J ( A e. y /\ ( F " y ) C_ x ) )
12 8 9 10 11 syl3anc 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> E. y e. J ( A e. y /\ ( F " y ) C_ x ) )
13 anass 
 |-  ( ( ( y e. J /\ A e. y ) /\ ( F " y ) C_ x ) <-> ( y e. J /\ ( A e. y /\ ( F " y ) C_ x ) ) )
14 simpl 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> A e. ( J fLim L ) )
15 flimtop 
 |-  ( A e. ( J fLim L ) -> J e. Top )
16 15 adantr 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> J e. Top )
17 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
18 16 17 sylib 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> J e. ( TopOn ` U. J ) )
19 1 flimfil 
 |-  ( A e. ( J fLim L ) -> L e. ( Fil ` U. J ) )
20 19 adantr 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> L e. ( Fil ` U. J ) )
21 flimopn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ L e. ( Fil ` U. J ) ) -> ( A e. ( J fLim L ) <-> ( A e. U. J /\ A. y e. J ( A e. y -> y e. L ) ) ) )
22 18 20 21 syl2anc 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( A e. ( J fLim L ) <-> ( A e. U. J /\ A. y e. J ( A e. y -> y e. L ) ) ) )
23 14 22 mpbid 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( A e. U. J /\ A. y e. J ( A e. y -> y e. L ) ) )
24 23 simprd 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> A. y e. J ( A e. y -> y e. L ) )
25 24 adantr 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> A. y e. J ( A e. y -> y e. L ) )
26 25 r19.21bi 
 |-  ( ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) /\ y e. J ) -> ( A e. y -> y e. L ) )
27 26 expimpd 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> ( ( y e. J /\ A e. y ) -> y e. L ) )
28 27 anim1d 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> ( ( ( y e. J /\ A e. y ) /\ ( F " y ) C_ x ) -> ( y e. L /\ ( F " y ) C_ x ) ) )
29 13 28 biimtrrid 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> ( ( y e. J /\ ( A e. y /\ ( F " y ) C_ x ) ) -> ( y e. L /\ ( F " y ) C_ x ) ) )
30 29 reximdv2 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> ( E. y e. J ( A e. y /\ ( F " y ) C_ x ) -> E. y e. L ( F " y ) C_ x ) )
31 12 30 mpd 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. K /\ ( F ` A ) e. x ) ) -> E. y e. L ( F " y ) C_ x )
32 31 expr 
 |-  ( ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. K ) -> ( ( F ` A ) e. x -> E. y e. L ( F " y ) C_ x ) )
33 32 ralrimiva 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> A. x e. K ( ( F ` A ) e. x -> E. y e. L ( F " y ) C_ x ) )
34 cnptop2 
 |-  ( F e. ( ( J CnP K ) ` A ) -> K e. Top )
35 34 adantl 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> K e. Top )
36 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
37 35 36 sylib 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> K e. ( TopOn ` U. K ) )
38 isflf 
 |-  ( ( K e. ( TopOn ` U. K ) /\ L e. ( Fil ` U. J ) /\ F : U. J --> U. K ) -> ( ( F ` A ) e. ( ( K fLimf L ) ` F ) <-> ( ( F ` A ) e. U. K /\ A. x e. K ( ( F ` A ) e. x -> E. y e. L ( F " y ) C_ x ) ) ) )
39 37 20 4 38 syl3anc 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( ( F ` A ) e. ( ( K fLimf L ) ` F ) <-> ( ( F ` A ) e. U. K /\ A. x e. K ( ( F ` A ) e. x -> E. y e. L ( F " y ) C_ x ) ) ) )
40 7 33 39 mpbir2and 
 |-  ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fLimf L ) ` F ) )