Metamath Proof Explorer

Theorem elfm

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

Ref Expression
Assertion elfm 
|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. B ( F " x ) C_ A ) ) )

Proof

Step Hyp Ref Expression
1 fmval 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( X filGen ran ( t e. B |-> ( F " t ) ) ) )
2 1 eleq2d 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> A e. ( X filGen ran ( t e. B |-> ( F " t ) ) ) ) )
3 eqid 
 |-  ran ( t e. B |-> ( F " t ) ) = ran ( t e. B |-> ( F " t ) )
4 3 fbasrn 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y --> X /\ X e. C ) -> ran ( t e. B |-> ( F " t ) ) e. ( fBas ` X ) )
5 4 3comr 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ran ( t e. B |-> ( F " t ) ) e. ( fBas ` X ) )
6 elfg 
 |-  ( ran ( t e. B |-> ( F " t ) ) e. ( fBas ` X ) -> ( A e. ( X filGen ran ( t e. B |-> ( F " t ) ) ) <-> ( A C_ X /\ E. y e. ran ( t e. B |-> ( F " t ) ) y C_ A ) ) )
7 5 6 syl 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( X filGen ran ( t e. B |-> ( F " t ) ) ) <-> ( A C_ X /\ E. y e. ran ( t e. B |-> ( F " t ) ) y C_ A ) ) )
8 simpr 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> x e. B )
9 eqid 
 |-  ( F " x ) = ( F " x )
10 imaeq2 
 |-  ( t = x -> ( F " t ) = ( F " x ) )
11 10 rspceeqv 
 |-  ( ( x e. B /\ ( F " x ) = ( F " x ) ) -> E. t e. B ( F " x ) = ( F " t ) )
12 8 9 11 sylancl 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> E. t e. B ( F " x ) = ( F " t ) )
13 simpl1 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> X e. C )
14 imassrn 
 |-  ( F " x ) C_ ran F
15 frn 
 |-  ( F : Y --> X -> ran F C_ X )
16 15 3ad2ant3 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ran F C_ X )
17 16 adantr 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> ran F C_ X )
18 14 17 sstrid 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> ( F " x ) C_ X )
19 13 18 ssexd 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> ( F " x ) e. _V )
20 eqid 
 |-  ( t e. B |-> ( F " t ) ) = ( t e. B |-> ( F " t ) )
21 20 elrnmpt 
 |-  ( ( F " x ) e. _V -> ( ( F " x ) e. ran ( t e. B |-> ( F " t ) ) <-> E. t e. B ( F " x ) = ( F " t ) ) )
22 19 21 syl 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> ( ( F " x ) e. ran ( t e. B |-> ( F " t ) ) <-> E. t e. B ( F " x ) = ( F " t ) ) )
23 12 22 mpbird 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ x e. B ) -> ( F " x ) e. ran ( t e. B |-> ( F " t ) ) )
24 10 cbvmptv 
 |-  ( t e. B |-> ( F " t ) ) = ( x e. B |-> ( F " x ) )
25 24 elrnmpt 
 |-  ( y e. ran ( t e. B |-> ( F " t ) ) -> ( y e. ran ( t e. B |-> ( F " t ) ) <-> E. x e. B y = ( F " x ) ) )
26 25 ibi 
 |-  ( y e. ran ( t e. B |-> ( F " t ) ) -> E. x e. B y = ( F " x ) )
27 26 adantl 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. ran ( t e. B |-> ( F " t ) ) ) -> E. x e. B y = ( F " x ) )
28 simpr 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y = ( F " x ) ) -> y = ( F " x ) )
29 28 sseq1d 
 |-  ( ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y = ( F " x ) ) -> ( y C_ A <-> ( F " x ) C_ A ) )
30 23 27 29 rexxfrd 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. y e. ran ( t e. B |-> ( F " t ) ) y C_ A <-> E. x e. B ( F " x ) C_ A ) )
31 30 anbi2d 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( A C_ X /\ E. y e. ran ( t e. B |-> ( F " t ) ) y C_ A ) <-> ( A C_ X /\ E. x e. B ( F " x ) C_ A ) ) )
32 2 7 31 3bitrd 
 |-  ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. B ( F " x ) C_ A ) ) )