Theorem fmfg

Description: The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

	Ref	Expression
Hypothesis	elfm2.l	⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion	fmfg	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		elfm2.l	⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
2	1	elfm2	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
3		fgcl	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
4	1 3	eqeltrid	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
5		filfbas	⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
6	4 5	syl	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
7		elfm	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
8	6 7	syl3an2	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
9	2 8	bitr4d	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
10	9	eqrdv	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )