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

Metamath Proof Explorer

Theorem foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006) (Proof shortened by AV, 29-Sep-2024)

Ref Expression
Assertion foco ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐹 : 𝐵 –onto→ 𝐶 )
2 fofun ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → Fun 𝐺 )
3 2 adantl ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → Fun 𝐺 )
4 forn ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ran 𝐺 = 𝐵 )
5 eqimss2 ⊢ ( ran 𝐺 = 𝐵 → 𝐵 ⊆ ran 𝐺 )
6 4 5 syl ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐵 ⊆ ran 𝐺 )
7 6 adantl ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐵 ⊆ ran 𝐺 )
8 focofo ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ Fun 𝐺 ∧ 𝐵 ⊆ ran 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –onto→ 𝐶 )
9 1 3 7 8 syl3anc ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –onto→ 𝐶 )
10 focnvimacdmdm ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )
11 10 eqcomd ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐴 = ( ◡ 𝐺 “ 𝐵 ) )
12 11 adantl ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐴 = ( ◡ 𝐺 “ 𝐵 ) )
13 foeq2 ⊢ ( 𝐴 = ( ◡ 𝐺 “ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –onto→ 𝐶 ) )
14 12 13 syl ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –onto→ 𝐶 ) )
15 9 14 mpbird ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 )