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 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∩ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ∩ ( 𝐹 “ 𝐵 ) )