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 ⊢ F Fn A ∧ B ⊆ A → ⋂ x ∈ B F ⁡ x = ⋂ F B

Proof

Step Hyp Ref Expression
1 fnssres ⊢ F Fn A ∧ B ⊆ A → F ↾ B Fn B
2 fniinfv ⊢ F ↾ B Fn B → ⋂ x ∈ B F ↾ B ⁡ x = ⋂ ran ⁡ F ↾ B
3 1 2 syl ⊢ F Fn A ∧ B ⊆ A → ⋂ x ∈ B F ↾ B ⁡ x = ⋂ ran ⁡ F ↾ B
4 fvres ⊢ x ∈ B → F ↾ B ⁡ x = F ⁡ x
5 4 iineq2i ⊢ ⋂ x ∈ B F ↾ B ⁡ x = ⋂ x ∈ B F ⁡ x
6 5 eqcomi ⊢ ⋂ x ∈ B F ⁡ x = ⋂ x ∈ B F ↾ B ⁡ x
7 df-ima ⊢ F B = ran ⁡ F ↾ B
8 7 inteqi ⊢ ⋂ F B = ⋂ ran ⁡ F ↾ B
9 3 6 8 3eqtr4g ⊢ F Fn A ∧ B ⊆ A → ⋂ x ∈ B F ⁡ x = ⋂ F B