Metamath Proof Explorer

Theorem elfm

Description: An element of a mapping filter. (Contributed by Jeff Hankins, 8-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion elfm ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fmval ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ) )
2 1 eleq2d ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ 𝐴 ∈ ( 𝑋 filGen ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ) ) )
3 eqid ⊢ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) = ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) )
4 3 fbasrn ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑋 ∈ 𝐶 ) → ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ∈ ( fBas ‘ 𝑋 ) )
5 4 3comr ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ∈ ( fBas ‘ 𝑋 ) )
6 elfg ⊢ ( ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) 𝑦 ⊆ 𝐴 ) ) )
7 5 6 syl ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) 𝑦 ⊆ 𝐴 ) ) )
8 simpr ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
9 eqid ⊢ ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑥 )
10 imaeq2 ⊢ ( 𝑡 = 𝑥 → ( 𝐹 “ 𝑡 ) = ( 𝐹 “ 𝑥 ) )
11 10 rspceeqv ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑥 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑡 ) )
12 8 9 11 sylancl ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑡 ∈ 𝐵 ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑡 ) )
13 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐶 )
14 imassrn ⊢ ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹
15 frn ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ran 𝐹 ⊆ 𝑋 )
16 15 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ran 𝐹 ⊆ 𝑋 )
17 16 adantr ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ran 𝐹 ⊆ 𝑋 )
18 14 17 sstrid ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑋 )
19 13 18 ssexd ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ∈ V )
20 eqid ⊢ ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) = ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) )
21 20 elrnmpt ⊢ ( ( 𝐹 “ 𝑥 ) ∈ V → ( ( 𝐹 “ 𝑥 ) ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑡 ) ) )
22 19 21 syl ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 “ 𝑥 ) ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑡 ) ) )
23 12 22 mpbird ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) )
24 10 cbvmptv ⊢ ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) )
25 24 elrnmpt ⊢ ( 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) → ( 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 “ 𝑥 ) ) )
26 25 ibi ⊢ ( 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 “ 𝑥 ) )
27 26 adantl ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 “ 𝑥 ) )
28 simpr ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) → 𝑦 = ( 𝐹 “ 𝑥 ) )
29 28 sseq1d ⊢ ( ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) → ( 𝑦 ⊆ 𝐴 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
30 23 27 29 rexxfrd ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) 𝑦 ⊆ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
31 30 anbi2d ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ ran ( 𝑡 ∈ 𝐵 ↦ ( 𝐹 “ 𝑡 ) ) 𝑦 ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
32 2 7 31 3bitrd ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )