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 ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion elfm2 ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elfm2.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
2 elfm ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
3 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
4 3 1 sseqtrrdi ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ 𝐿 )
5 4 sselda ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐿 )
6 5 adantrr ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ∈ 𝐿 )
7 6 3ad2antl2 ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ∈ 𝐿 )
8 simprr ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐹 “ 𝑦 ) ⊆ 𝐴 )
9 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
10 9 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ↔ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
11 10 rspcev ⊢ ( ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )
12 7 8 11 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )
13 12 rexlimdvaa ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 → ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
14 1 eleq2i ⊢ ( 𝑥 ∈ 𝐿 ↔ 𝑥 ∈ ( 𝑌 filGen 𝐵 ) )
15 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑥 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) )
16 14 15 bitrid ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑥 ∈ 𝐿 ↔ ( 𝑥 ⊆ 𝑌 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) )
17 16 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ 𝐿 ↔ ( 𝑥 ⊆ 𝑌 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) )
18 imass2 ⊢ ( 𝑦 ⊆ 𝑥 → ( 𝐹 “ 𝑦 ) ⊆ ( 𝐹 “ 𝑥 ) )
19 sstr2 ⊢ ( ( 𝐹 “ 𝑦 ) ⊆ ( 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
20 19 com12 ⊢ ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ( ( 𝐹 “ 𝑦 ) ⊆ ( 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
21 20 ad2antll ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝑦 ) ⊆ ( 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
22 18 21 syl5 ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) → ( 𝑦 ⊆ 𝑥 → ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
23 22 reximdv ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
24 23 expr ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
25 24 com23 ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
26 25 expimpd ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑥 ⊆ 𝑌 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
27 17 26 sylbid ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ 𝐿 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ) )
28 27 rexlimdv ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) )
29 13 28 impbid ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ↔ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
30 29 anbi2d ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝐹 “ 𝑦 ) ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
31 2 30 bitrd ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )