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

Metamath Proof Explorer

Theorem fvco4i

Description: Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Hypotheses fvco4i.a ⊢ ∅ = ( 𝐹 ‘ ∅ )
fvco4i.b ⊢ Fun 𝐺
Assertion fvco4i ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fvco4i.a ⊢ ∅ = ( 𝐹 ‘ ∅ )
2 fvco4i.b ⊢ Fun 𝐺
3 funfn ⊢ ( Fun 𝐺 ↔ 𝐺 Fn dom 𝐺 )
4 2 3 mpbi ⊢ 𝐺 Fn dom 𝐺
5 fvco2 ⊢ ( ( 𝐺 Fn dom 𝐺 ∧ 𝑋 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
6 4 5 mpan ⊢ ( 𝑋 ∈ dom 𝐺 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
7 dmcoss ⊢ dom ( 𝐹 ∘ 𝐺 ) ⊆ dom 𝐺
8 7 sseli ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → 𝑋 ∈ dom 𝐺 )
9 ndmfv ⊢ ( ¬ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ∅ )
10 8 9 nsyl5 ⊢ ( ¬ 𝑋 ∈ dom 𝐺 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ∅ )
11 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑋 ) = ∅ )
12 11 fveq2d ⊢ ( ¬ 𝑋 ∈ dom 𝐺 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ ∅ ) )
13 1 10 12 3eqtr4a ⊢ ( ¬ 𝑋 ∈ dom 𝐺 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
14 6 13 pm2.61i ⊢ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) )