Metamath Proof Explorer

Theorem elfm2

Description: An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis elfm2.l 
|- L = ( Y filGen B )
Assertion elfm2 
|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. L ( F " x ) C_ A ) ) )

Proof

Step Hyp Ref Expression
1 elfm2.l 
 |-  L = ( Y filGen B )
2 elfm 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. y e. B ( F " y ) C_ A ) ) )
3 ssfg 
 |-  ( B e. ( fBas ` Y ) -> B C_ ( Y filGen B ) )
4 3 1 sseqtrrdi 
 |-  ( B e. ( fBas ` Y ) -> B C_ L )
5 4 sselda 
 |-  ( ( B e. ( fBas ` Y ) /\ y e. B ) -> y e. L )
6 5 adantrr 
 |-  ( ( B e. ( fBas ` Y ) /\ ( y e. B /\ ( F " y ) C_ A ) ) -> y e. L )
7 6 3ad2antl2 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( y e. B /\ ( F " y ) C_ A ) ) -> y e. L )
8 simprr 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( y e. B /\ ( F " y ) C_ A ) ) -> ( F " y ) C_ A )
9 imaeq2 
 |-  ( x = y -> ( F " x ) = ( F " y ) )
10 9 sseq1d 
 |-  ( x = y -> ( ( F " x ) C_ A <-> ( F " y ) C_ A ) )
11 10 rspcev 
 |-  ( ( y e. L /\ ( F " y ) C_ A ) -> E. x e. L ( F " x ) C_ A )
12 7 8 11 syl2anc 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( y e. B /\ ( F " y ) C_ A ) ) -> E. x e. L ( F " x ) C_ A )
13 12 rexlimdvaa 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. y e. B ( F " y ) C_ A -> E. x e. L ( F " x ) C_ A ) )
14 1 eleq2i 
 |-  ( x e. L <-> x e. ( Y filGen B ) )
15 elfg 
 |-  ( B e. ( fBas ` Y ) -> ( x e. ( Y filGen B ) <-> ( x C_ Y /\ E. y e. B y C_ x ) ) )
16 14 15 syl5bb 
 |-  ( B e. ( fBas ` Y ) -> ( x e. L <-> ( x C_ Y /\ E. y e. B y C_ x ) ) )
17 16 3ad2ant2 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. L <-> ( x C_ Y /\ E. y e. B y C_ x ) ) )
18 imass2 
 |-  ( y C_ x -> ( F " y ) C_ ( F " x ) )
19 sstr2 
 |-  ( ( F " y ) C_ ( F " x ) -> ( ( F " x ) C_ A -> ( F " y ) C_ A ) )
20 19 com12 
 |-  ( ( F " x ) C_ A -> ( ( F " y ) C_ ( F " x ) -> ( F " y ) C_ A ) )
21 20 ad2antll 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( x C_ Y /\ ( F " x ) C_ A ) ) -> ( ( F " y ) C_ ( F " x ) -> ( F " y ) C_ A ) )
22 18 21 syl5 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( x C_ Y /\ ( F " x ) C_ A ) ) -> ( y C_ x -> ( F " y ) C_ A ) )
23 22 reximdv 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ ( x C_ Y /\ ( F " x ) C_ A ) ) -> ( E. y e. B y C_ x -> E. y e. B ( F " y ) C_ A ) )
24 23 expr 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x C_ Y ) -> ( ( F " x ) C_ A -> ( E. y e. B y C_ x -> E. y e. B ( F " y ) C_ A ) ) )
25 24 com23 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x C_ Y ) -> ( E. y e. B y C_ x -> ( ( F " x ) C_ A -> E. y e. B ( F " y ) C_ A ) ) )
26 25 expimpd 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( x C_ Y /\ E. y e. B y C_ x ) -> ( ( F " x ) C_ A -> E. y e. B ( F " y ) C_ A ) ) )
27 17 26 sylbid 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. L -> ( ( F " x ) C_ A -> E. y e. B ( F " y ) C_ A ) ) )
28 27 rexlimdv 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. x e. L ( F " x ) C_ A -> E. y e. B ( F " y ) C_ A ) )
29 13 28 impbid 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. y e. B ( F " y ) C_ A <-> E. x e. L ( F " x ) C_ A ) )
30 29 anbi2d 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( A C_ X /\ E. y e. B ( F " y ) C_ A ) <-> ( A C_ X /\ E. x e. L ( F " x ) C_ A ) ) )
31 2 30 bitrd 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. L ( F " x ) C_ A ) ) )