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	⊢ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) )