Theorem funco

Description: The composition of two functions is a function. Exercise 29 of TakeutiZaring p. 25. (Contributed by NM, 26-Jan-1997) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	funco	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		funmo	⊢ ( Fun 𝐺 → ∃* 𝑧 𝑥 𝐺 𝑧 )
2		funmo	⊢ ( Fun 𝐹 → ∃* 𝑦 𝑧 𝐹 𝑦 )
3	2	alrimiv	⊢ ( Fun 𝐹 → ∀ 𝑧 ∃* 𝑦 𝑧 𝐹 𝑦 )
4		moexexvw	⊢ ( ( ∃* 𝑧 𝑥 𝐺 𝑧 ∧ ∀ 𝑧 ∃* 𝑦 𝑧 𝐹 𝑦 ) → ∃* 𝑦 ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) )
5	1 3 4	syl2anr	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ∃* 𝑦 ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) )
6	5	alrimiv	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ∀ 𝑥 ∃* 𝑦 ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) )
7		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) } ↔ ∀ 𝑥 ∃* 𝑦 ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) )
8	6 7	sylibr	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) } )
9		df-co	⊢ ( 𝐹 ∘ 𝐺 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) }
10	9	funeqi	⊢ ( Fun ( 𝐹 ∘ 𝐺 ) ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) } )
11	8 10	sylibr	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )