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 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion elfm3 ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 elfm2.l 𝐿 = ( 𝑌 filGen 𝐵 )
2 foima ( 𝐹 : 𝑌onto𝑋 → ( 𝐹𝑌 ) = 𝑋 )
3 2 adantl ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐹𝑌 ) = 𝑋 )
4 fofun ( 𝐹 : 𝑌onto𝑋 → Fun 𝐹 )
5 elfvdm ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
6 funimaexg ( ( Fun 𝐹𝑌 ∈ dom fBas ) → ( 𝐹𝑌 ) ∈ V )
7 4 5 6 syl2anr ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐹𝑌 ) ∈ V )
8 3 7 eqeltrrd ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → 𝑋 ∈ V )
9 fof ( 𝐹 : 𝑌onto𝑋𝐹 : 𝑌𝑋 )
10 1 elfm2 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) ) )
11 9 10 syl3an3 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) ) )
12 fgcl ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
13 1 12 eqeltrid ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
14 13 3ad2ant2 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
15 14 ad2antrr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
16 simprl ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → 𝑦𝐿 )
17 cnvimass ( 𝐹𝐴 ) ⊆ dom 𝐹
18 fofn ( 𝐹 : 𝑌onto𝑋𝐹 Fn 𝑌 )
19 18 fndmd ( 𝐹 : 𝑌onto𝑋 → dom 𝐹 = 𝑌 )
20 17 19 sseqtrid ( 𝐹 : 𝑌onto𝑋 → ( 𝐹𝐴 ) ⊆ 𝑌 )
21 20 3ad2ant3 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐹𝐴 ) ⊆ 𝑌 )
22 21 ad2antrr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → ( 𝐹𝐴 ) ⊆ 𝑌 )
23 4 3ad2ant3 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → Fun 𝐹 )
24 23 ad2antrr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝐿 ) → Fun 𝐹 )
25 1 eleq2i ( 𝑦𝐿𝑦 ∈ ( 𝑌 filGen 𝐵 ) )
26 elfg ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦𝑌 ∧ ∃ 𝑧𝐵 𝑧𝑦 ) ) )
27 26 3ad2ant2 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦𝑌 ∧ ∃ 𝑧𝐵 𝑧𝑦 ) ) )
28 27 adantr ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦𝑌 ∧ ∃ 𝑧𝐵 𝑧𝑦 ) ) )
29 25 28 syl5bb ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) → ( 𝑦𝐿 ↔ ( 𝑦𝑌 ∧ ∃ 𝑧𝐵 𝑧𝑦 ) ) )
30 29 simprbda ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝐿 ) → 𝑦𝑌 )
31 sseq2 ( dom 𝐹 = 𝑌 → ( 𝑦 ⊆ dom 𝐹𝑦𝑌 ) )
32 31 biimpar ( ( dom 𝐹 = 𝑌𝑦𝑌 ) → 𝑦 ⊆ dom 𝐹 )
33 19 32 sylan ( ( 𝐹 : 𝑌onto𝑋𝑦𝑌 ) → 𝑦 ⊆ dom 𝐹 )
34 33 3ad2antl3 ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝑦𝑌 ) → 𝑦 ⊆ dom 𝐹 )
35 34 adantlr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝑌 ) → 𝑦 ⊆ dom 𝐹 )
36 30 35 syldan ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝐿 ) → 𝑦 ⊆ dom 𝐹 )
37 funimass3 ( ( Fun 𝐹𝑦 ⊆ dom 𝐹 ) → ( ( 𝐹𝑦 ) ⊆ 𝐴𝑦 ⊆ ( 𝐹𝐴 ) ) )
38 24 36 37 syl2anc ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝐿 ) → ( ( 𝐹𝑦 ) ⊆ 𝐴𝑦 ⊆ ( 𝐹𝐴 ) ) )
39 38 biimpd ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ 𝑦𝐿 ) → ( ( 𝐹𝑦 ) ⊆ 𝐴𝑦 ⊆ ( 𝐹𝐴 ) ) )
40 39 impr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ⊆ ( 𝐹𝐴 ) )
41 filss ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝐴 ) ⊆ 𝑌𝑦 ⊆ ( 𝐹𝐴 ) ) ) → ( 𝐹𝐴 ) ∈ 𝐿 )
42 15 16 22 40 41 syl13anc ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → ( 𝐹𝐴 ) ∈ 𝐿 )
43 foimacnv ( ( 𝐹 : 𝑌onto𝑋𝐴𝑋 ) → ( 𝐹 “ ( 𝐹𝐴 ) ) = 𝐴 )
44 43 eqcomd ( ( 𝐹 : 𝑌onto𝑋𝐴𝑋 ) → 𝐴 = ( 𝐹 “ ( 𝐹𝐴 ) ) )
45 44 3ad2antl3 ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) → 𝐴 = ( 𝐹 “ ( 𝐹𝐴 ) ) )
46 45 adantr ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → 𝐴 = ( 𝐹 “ ( 𝐹𝐴 ) ) )
47 imaeq2 ( 𝑥 = ( 𝐹𝐴 ) → ( 𝐹𝑥 ) = ( 𝐹 “ ( 𝐹𝐴 ) ) )
48 47 rspceeqv ( ( ( 𝐹𝐴 ) ∈ 𝐿𝐴 = ( 𝐹 “ ( 𝐹𝐴 ) ) ) → ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) )
49 42 46 48 syl2anc ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) ∧ ( 𝑦𝐿 ∧ ( 𝐹𝑦 ) ⊆ 𝐴 ) ) → ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) )
50 49 rexlimdvaa ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ 𝐴𝑋 ) → ( ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 → ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )
51 50 expimpd ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) → ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )
52 simprr ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → 𝐴 = ( 𝐹𝑥 ) )
53 imassrn ( 𝐹𝑥 ) ⊆ ran 𝐹
54 forn ( 𝐹 : 𝑌onto𝑋 → ran 𝐹 = 𝑋 )
55 54 3ad2ant3 ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ran 𝐹 = 𝑋 )
56 55 adantr ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → ran 𝐹 = 𝑋 )
57 53 56 sseqtrid ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → ( 𝐹𝑥 ) ⊆ 𝑋 )
58 52 57 eqsstrd ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → 𝐴𝑋 )
59 eqimss2 ( 𝐴 = ( 𝐹𝑥 ) → ( 𝐹𝑥 ) ⊆ 𝐴 )
60 imaeq2 ( 𝑦 = 𝑥 → ( 𝐹𝑦 ) = ( 𝐹𝑥 ) )
61 60 sseq1d ( 𝑦 = 𝑥 → ( ( 𝐹𝑦 ) ⊆ 𝐴 ↔ ( 𝐹𝑥 ) ⊆ 𝐴 ) )
62 61 rspcev ( ( 𝑥𝐿 ∧ ( 𝐹𝑥 ) ⊆ 𝐴 ) → ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 )
63 59 62 sylan2 ( ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) → ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 )
64 63 adantl ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 )
65 58 64 jca ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) ∧ ( 𝑥𝐿𝐴 = ( 𝐹𝑥 ) ) ) → ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) )
66 65 rexlimdvaa ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) → ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) ) )
67 51 66 impbid ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( ( 𝐴𝑋 ∧ ∃ 𝑦𝐿 ( 𝐹𝑦 ) ⊆ 𝐴 ) ↔ ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )
68 11 67 bitrd ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )
69 68 3coml ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋𝑋 ∈ V ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )
70 8 69 mpd3an3 ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌onto𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥𝐿 𝐴 = ( 𝐹𝑥 ) ) )