This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imaiinfv

Description: Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion imaiinfv ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∩ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ∩ ( 𝐹 “ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
2 fniinfv ⊢ ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 → ∩ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ∩ ran ( 𝐹 ↾ 𝐵 ) )
3 1 2 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∩ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ∩ ran ( 𝐹 ↾ 𝐵 ) )
4 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
5 4 iineq2i ⊢ ∩ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ∩ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 )
6 5 eqcomi ⊢ ∩ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ∩ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 )
7 df-ima ⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
8 7 inteqi ⊢ ∩ ( 𝐹 “ 𝐵 ) = ∩ ran ( 𝐹 ↾ 𝐵 )
9 3 6 8 3eqtr4g ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∩ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ∩ ( 𝐹 “ 𝐵 ) )