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→ 𝐶 )