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

Metamath Proof Explorer

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 ( 𝐹 ∘ 𝐺 ) )