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

Metamath Proof Explorer

Theorem dfimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion dfimafn2 ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 { ( 𝐹 ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dfimafn ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
2 iunab ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 }
3 1 2 eqtr4di ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
4 df-sn ⊢ { ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∣ 𝑦 = ( 𝐹 ‘ 𝑥 ) }
5 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
6 5 abbii ⊢ { 𝑦 ∣ 𝑦 = ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 }
7 4 6 eqtri ⊢ { ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 }
8 7 a1i ⊢ ( 𝑥 ∈ 𝐴 → { ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
9 8 iuneq2i ⊢ ∪ 𝑥 ∈ 𝐴 { ( 𝐹 ‘ 𝑥 ) } = ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝐹 ‘ 𝑥 ) = 𝑦 }
10 3 9 eqtr4di ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 { ( 𝐹 ‘ 𝑥 ) } )