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

Metamath Proof Explorer

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