Theorem foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006)

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

Proof

Step	Hyp	Ref	Expression
1		dffo2	⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) )
2		dffo2	⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 ↔ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) )
3		fco	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
4	3	ad2ant2r	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
5		fdm	⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → dom 𝐹 = 𝐵 )
6		eqtr3	⊢ ( ( dom 𝐹 = 𝐵 ∧ ran 𝐺 = 𝐵 ) → dom 𝐹 = ran 𝐺 )
7	5 6	sylan	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐺 = 𝐵 ) → dom 𝐹 = ran 𝐺 )
8		rncoeq	⊢ ( dom 𝐹 = ran 𝐺 → ran ( 𝐹 ∘ 𝐺 ) = ran 𝐹 )
9	8	eqeq1d	⊢ ( dom 𝐹 = ran 𝐺 → ( ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ↔ ran 𝐹 = 𝐶 ) )
10	9	biimpar	⊢ ( ( dom 𝐹 = ran 𝐺 ∧ ran 𝐹 = 𝐶 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 )
11	7 10	sylan	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐺 = 𝐵 ) ∧ ran 𝐹 = 𝐶 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 )
12	11	an32s	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ran 𝐺 = 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 )
13	12	adantrl	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 )
14	4 13	jca	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) )
15	1 2 14	syl2anb	⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) )
16		dffo2	⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ↔ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) )
17	15 16	sylibr	⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 )