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

Metamath Proof Explorer

Theorem fvco2

Description: Value of a function composition. Similar to second part of Theorem 3H of Enderton p. 47. (Contributed by NM, 9-Oct-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion fvco2 ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 imaco ⊢ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) = ( 𝐹 “ ( 𝐺 “ { 𝑋 } ) )
2 fnsnfv ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → { ( 𝐺 ‘ 𝑋 ) } = ( 𝐺 “ { 𝑋 } ) )
3 2 imaeq2d ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 “ { ( 𝐺 ‘ 𝑋 ) } ) = ( 𝐹 “ ( 𝐺 “ { 𝑋 } ) ) )
4 1 3 eqtr4id ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) = ( 𝐹 “ { ( 𝐺 ‘ 𝑋 ) } ) )
5 4 eleq2d ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ↔ 𝑥 ∈ ( 𝐹 “ { ( 𝐺 ‘ 𝑋 ) } ) ) )
6 5 iotabidv ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐺 ‘ 𝑋 ) } ) ) )
7 dffv3 ⊢ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) )
8 dffv3 ⊢ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐺 ‘ 𝑋 ) } ) )
9 6 7 8 3eqtr4g ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )