Theorem intimafv

Description: The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024)

	Ref	Expression
Assertion	intimafv	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ∩ ( 𝐹 “ 𝐴 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dfimafn	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
2	1	inteqd	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ∩ ( 𝐹 “ 𝐴 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
3		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ V
5		iinabrex	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ V → ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
6	4 5	ax-mp	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
7		eqcom	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) )
8	7	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
9	8	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
10	9	inteqi	⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 } = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
11	6 10	eqtr4i	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 }
12	2 11	eqtr4di	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ∩ ( 𝐹 “ 𝐴 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )