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=YfilGenB
Assertion elfm2 ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→A∈XFilMapF⁡B↔A⊆X∧∃x∈LFx⊆A

Proof

Step Hyp Ref Expression
1 elfm2.l ⊢L=YfilGenB
2 elfm ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→A∈XFilMapF⁡B↔A⊆X∧∃y∈BFy⊆A
3 ssfg ⊢B∈fBas⁡Y→B⊆YfilGenB
4 3 1 sseqtrrdi ⊢B∈fBas⁡Y→B⊆L
5 4 sselda ⊢B∈fBas⁡Y∧y∈B→y∈L
6 5 adantrr ⊢B∈fBas⁡Y∧y∈B∧Fy⊆A→y∈L
7 6 3ad2antl2 ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧y∈B∧Fy⊆A→y∈L
8 simprr ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧y∈B∧Fy⊆A→Fy⊆A
9 imaeq2 ⊢x=y→Fx=Fy
10 9 sseq1d ⊢x=y→Fx⊆A↔Fy⊆A
11 10 rspcev ⊢y∈L∧Fy⊆A→∃x∈LFx⊆A
12 7 8 11 syl2anc ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧y∈B∧Fy⊆A→∃x∈LFx⊆A
13 12 rexlimdvaa ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→∃y∈BFy⊆A→∃x∈LFx⊆A
14 1 eleq2i ⊢x∈L↔x∈YfilGenB
15 elfg ⊢B∈fBas⁡Y→x∈YfilGenB↔x⊆Y∧∃y∈By⊆x
16 14 15 bitrid ⊢B∈fBas⁡Y→x∈L↔x⊆Y∧∃y∈By⊆x
17 16 3ad2ant2 ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→x∈L↔x⊆Y∧∃y∈By⊆x
18 imass2 ⊢y⊆x→Fy⊆Fx
19 sstr2 ⊢Fy⊆Fx→Fx⊆A→Fy⊆A
20 19 com12 ⊢Fx⊆A→Fy⊆Fx→Fy⊆A
21 20 ad2antll ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧x⊆Y∧Fx⊆A→Fy⊆Fx→Fy⊆A
22 18 21 syl5 ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧x⊆Y∧Fx⊆A→y⊆x→Fy⊆A
23 22 reximdv ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧x⊆Y∧Fx⊆A→∃y∈By⊆x→∃y∈BFy⊆A
24 23 expr ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧x⊆Y→Fx⊆A→∃y∈By⊆x→∃y∈BFy⊆A
25 24 com23 ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X∧x⊆Y→∃y∈By⊆x→Fx⊆A→∃y∈BFy⊆A
26 25 expimpd ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→x⊆Y∧∃y∈By⊆x→Fx⊆A→∃y∈BFy⊆A
27 17 26 sylbid ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→x∈L→Fx⊆A→∃y∈BFy⊆A
28 27 rexlimdv ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→∃x∈LFx⊆A→∃y∈BFy⊆A
29 13 28 impbid ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→∃y∈BFy⊆A↔∃x∈LFx⊆A
30 29 anbi2d ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→A⊆X∧∃y∈BFy⊆A↔A⊆X∧∃x∈LFx⊆A
31 2 30 bitrd ⊢X∈C∧B∈fBas⁡Y∧F:Y⟶X→A∈XFilMapF⁡B↔A⊆X∧∃x∈LFx⊆A