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 fndm ⊢ ( 𝐹 Fn 𝑌 → dom 𝐹 = 𝑌 )
20 18 19 syl ⊢ ( 𝐹 : 𝑌 –onto→ 𝑋 → dom 𝐹 = 𝑌 )
21 17 20 sseqtrid ⊢ ( 𝐹 : 𝑌 –onto→ 𝑋 → ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝑌 )
22 21 3ad2ant3 ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝑌 )
23 22 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝑌 )
24 4 3ad2ant3 ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → Fun 𝐹 )
25 24 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ) → Fun 𝐹 )
26 1 eleq2i ⊢ ( 𝑦 ∈ 𝐿 ↔ 𝑦 ∈ ( 𝑌 filGen 𝐵 ) )
27 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐵 𝑧 ⊆ 𝑦 ) ) )
28 27 3ad2ant2 ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐵 𝑧 ⊆ 𝑦 ) ) )
29 28 adantr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑦 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐵 𝑧 ⊆ 𝑦 ) ) )
30 26 29 syl5bb ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑦 ∈ 𝐿 ↔ ( 𝑦 ⊆ 𝑌 ∧ ∃ 𝑧 ∈ 𝐵 𝑧 ⊆ 𝑦 ) ) )
31 30 simprbda ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ) → 𝑦 ⊆ 𝑌 )
32 sseq2 ⊢ ( dom 𝐹 = 𝑌 → ( 𝑦 ⊆ dom 𝐹 ↔ 𝑦 ⊆ 𝑌 ) )
33 32 biimpar ⊢ ( ( dom 𝐹 = 𝑌 ∧ 𝑦 ⊆ 𝑌 ) → 𝑦 ⊆ dom 𝐹 )
34 20 33 sylan ⊢ ( ( 𝐹 : 𝑌 –onto→ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) → 𝑦 ⊆ dom 𝐹 )
35 34 3ad2antl3 ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝑦 ⊆ 𝑌 ) → 𝑦 ⊆ dom 𝐹 )
36 35 adantlr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ⊆ 𝑌 ) → 𝑦 ⊆ dom 𝐹 )
37 31 36 syldan ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ) → 𝑦 ⊆ dom 𝐹 )
38 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑦 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ↔ 𝑦 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
39 25 37 38 syl2anc ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ↔ 𝑦 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
40 39 biimpd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝐴 → 𝑦 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
41 40 impr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
42 filss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝑌 ∧ 𝑦 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐿 )
43 15 16 23 41 42 syl13anc ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐿 )
44 foimacnv ⊢ ( ( 𝐹 : 𝑌 –onto→ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) = 𝐴 )
45 44 eqcomd ⊢ ( ( 𝐹 : 𝑌 –onto→ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) )
46 45 3ad2antl3 ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) )
47 46 adantr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → 𝐴 = ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) )
48 imaeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝐴 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) )
49 48 rspceeqv ⊢ ( ( ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ ( ◡ 𝐹 “ 𝐴 ) ) ) → ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) )
50 43 47 49 syl2anc ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) )
51 50 rexlimdvaa ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 → ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )
52 51 expimpd ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )
53 simprr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → 𝐴 = ( 𝐹 “ 𝑥 ) )
54 imassrn ⊢ ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹
55 forn ⊢ ( 𝐹 : 𝑌 –onto→ 𝑋 → ran 𝐹 = 𝑋 )
56 55 3ad2ant3 ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ran 𝐹 = 𝑋 )
57 56 adantr ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → ran 𝐹 = 𝑋 )
58 54 57 sseqtrid ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑋 )
59 53 58 eqsstrd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → 𝐴 ⊆ 𝑋 )
60 eqimss2 ⊢ ( 𝐴 = ( 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )
61 imaeq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 “ 𝑦 ) = ( 𝐹 “ 𝑥 ) )
62 61 sseq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
63 62 rspcev ⊢ ( ( 𝑥 ∈ 𝐿 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 )
64 60 63 sylan2 ⊢ ( ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 )
65 64 adantl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 )
66 59 65 jca ⊢ ( ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) ∧ ( 𝑥 ∈ 𝐿 ∧ 𝐴 = ( 𝐹 “ 𝑥 ) ) ) → ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
67 66 rexlimdvaa ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) → ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
68 52 67 impbid ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )
69 11 68 bitrd ⊢ ( ( 𝑋 ∈ V ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )
70 69 3coml ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ∧ 𝑋 ∈ V ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )
71 8 70 mpd3an3 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 –onto→ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐿 𝐴 = ( 𝐹 “ 𝑥 ) ) )