Metamath Proof Explorer

Theorem elfm3

Description: An alternate formulation of elementhood in a mapping filter that requires F to be onto. (Contributed by Jeff Hankins, 1-Oct-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 elfm2.l 
 |-  L = ( Y filGen B )
2 foima 
 |-  ( F : Y -onto-> X -> ( F " Y ) = X )
3 2 adantl 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( F " Y ) = X )
4 fofun 
 |-  ( F : Y -onto-> X -> Fun F )
5 elfvdm 
 |-  ( B e. ( fBas ` Y ) -> Y e. dom fBas )
6 funimaexg 
 |-  ( ( Fun F /\ Y e. dom fBas ) -> ( F " Y ) e. _V )
7 4 5 6 syl2anr 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( F " Y ) e. _V )
8 3 7 eqeltrrd 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> X e. _V )
9 fof 
 |-  ( F : Y -onto-> X -> F : Y --> X )
10 1 elfm2 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. y e. L ( F " y ) C_ A ) ) )
11 9 10 syl3an3 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. y e. L ( F " y ) C_ A ) ) )
12 fgcl 
 |-  ( B e. ( fBas ` Y ) -> ( Y filGen B ) e. ( Fil ` Y ) )
13 1 12 eqeltrid 
 |-  ( B e. ( fBas ` Y ) -> L e. ( Fil ` Y ) )
14 13 3ad2ant2 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> L e. ( Fil ` Y ) )
15 14 ad2antrr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> L e. ( Fil ` Y ) )
16 simprl 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> y e. L )
17 cnvimass 
 |-  ( `' F " A ) C_ dom F
18 fofn 
 |-  ( F : Y -onto-> X -> F Fn Y )
19 18 fndmd 
 |-  ( F : Y -onto-> X -> dom F = Y )
20 17 19 sseqtrid 
 |-  ( F : Y -onto-> X -> ( `' F " A ) C_ Y )
21 20 3ad2ant3 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( `' F " A ) C_ Y )
22 21 ad2antrr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> ( `' F " A ) C_ Y )
23 4 3ad2ant3 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> Fun F )
24 23 ad2antrr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y e. L ) -> Fun F )
25 1 eleq2i 
 |-  ( y e. L <-> y e. ( Y filGen B ) )
26 elfg 
 |-  ( B e. ( fBas ` Y ) -> ( y e. ( Y filGen B ) <-> ( y C_ Y /\ E. z e. B z C_ y ) ) )
27 26 3ad2ant2 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( y e. ( Y filGen B ) <-> ( y C_ Y /\ E. z e. B z C_ y ) ) )
28 27 adantr 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) -> ( y e. ( Y filGen B ) <-> ( y C_ Y /\ E. z e. B z C_ y ) ) )
29 25 28 syl5bb 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) -> ( y e. L <-> ( y C_ Y /\ E. z e. B z C_ y ) ) )
30 29 simprbda 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y e. L ) -> y C_ Y )
31 sseq2 
 |-  ( dom F = Y -> ( y C_ dom F <-> y C_ Y ) )
32 31 biimpar 
 |-  ( ( dom F = Y /\ y C_ Y ) -> y C_ dom F )
33 19 32 sylan 
 |-  ( ( F : Y -onto-> X /\ y C_ Y ) -> y C_ dom F )
34 33 3ad2antl3 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ y C_ Y ) -> y C_ dom F )
35 34 adantlr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y C_ Y ) -> y C_ dom F )
36 30 35 syldan 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y e. L ) -> y C_ dom F )
37 funimass3 
 |-  ( ( Fun F /\ y C_ dom F ) -> ( ( F " y ) C_ A <-> y C_ ( `' F " A ) ) )
38 24 36 37 syl2anc 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y e. L ) -> ( ( F " y ) C_ A <-> y C_ ( `' F " A ) ) )
39 38 biimpd 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ y e. L ) -> ( ( F " y ) C_ A -> y C_ ( `' F " A ) ) )
40 39 impr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> y C_ ( `' F " A ) )
41 filss 
 |-  ( ( L e. ( Fil ` Y ) /\ ( y e. L /\ ( `' F " A ) C_ Y /\ y C_ ( `' F " A ) ) ) -> ( `' F " A ) e. L )
42 15 16 22 40 41 syl13anc 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> ( `' F " A ) e. L )
43 foimacnv 
 |-  ( ( F : Y -onto-> X /\ A C_ X ) -> ( F " ( `' F " A ) ) = A )
44 43 eqcomd 
 |-  ( ( F : Y -onto-> X /\ A C_ X ) -> A = ( F " ( `' F " A ) ) )
45 44 3ad2antl3 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) -> A = ( F " ( `' F " A ) ) )
46 45 adantr 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> A = ( F " ( `' F " A ) ) )
47 imaeq2 
 |-  ( x = ( `' F " A ) -> ( F " x ) = ( F " ( `' F " A ) ) )
48 47 rspceeqv 
 |-  ( ( ( `' F " A ) e. L /\ A = ( F " ( `' F " A ) ) ) -> E. x e. L A = ( F " x ) )
49 42 46 48 syl2anc 
 |-  ( ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) /\ ( y e. L /\ ( F " y ) C_ A ) ) -> E. x e. L A = ( F " x ) )
50 49 rexlimdvaa 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ A C_ X ) -> ( E. y e. L ( F " y ) C_ A -> E. x e. L A = ( F " x ) ) )
51 50 expimpd 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( ( A C_ X /\ E. y e. L ( F " y ) C_ A ) -> E. x e. L A = ( F " x ) ) )
52 simprr 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> A = ( F " x ) )
53 imassrn 
 |-  ( F " x ) C_ ran F
54 forn 
 |-  ( F : Y -onto-> X -> ran F = X )
55 54 3ad2ant3 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ran F = X )
56 55 adantr 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> ran F = X )
57 53 56 sseqtrid 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> ( F " x ) C_ X )
58 52 57 eqsstrd 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> A C_ X )
59 eqimss2 
 |-  ( A = ( F " x ) -> ( F " x ) C_ A )
60 imaeq2 
 |-  ( y = x -> ( F " y ) = ( F " x ) )
61 60 sseq1d 
 |-  ( y = x -> ( ( F " y ) C_ A <-> ( F " x ) C_ A ) )
62 61 rspcev 
 |-  ( ( x e. L /\ ( F " x ) C_ A ) -> E. y e. L ( F " y ) C_ A )
63 59 62 sylan2 
 |-  ( ( x e. L /\ A = ( F " x ) ) -> E. y e. L ( F " y ) C_ A )
64 63 adantl 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> E. y e. L ( F " y ) C_ A )
65 58 64 jca 
 |-  ( ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) /\ ( x e. L /\ A = ( F " x ) ) ) -> ( A C_ X /\ E. y e. L ( F " y ) C_ A ) )
66 65 rexlimdvaa 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( E. x e. L A = ( F " x ) -> ( A C_ X /\ E. y e. L ( F " y ) C_ A ) ) )
67 51 66 impbid 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( ( A C_ X /\ E. y e. L ( F " y ) C_ A ) <-> E. x e. L A = ( F " x ) ) )
68 11 67 bitrd 
 |-  ( ( X e. _V /\ B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> E. x e. L A = ( F " x ) ) )
69 68 3coml 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X /\ X e. _V ) -> ( A e. ( ( X FilMap F ) ` B ) <-> E. x e. L A = ( F " x ) ) )
70 8 69 mpd3an3 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> E. x e. L A = ( F " x ) ) )