Theorem foco2

Description: If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		foelrn	⊢ ( ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) )
2		ffvelrn	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐵 )
3		fvco3	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
4		fveq2	⊢ ( 𝑥 = ( 𝐺 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
5	4	rspceeqv	⊢ ( ( ( 𝐺 ‘ 𝑧 ) ∈ 𝐵 ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
6	2 3 5	syl2anc	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
7		eqeq1	⊢ ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
8	7	rexbidv	⊢ ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
9	6 8	syl5ibrcom	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
10	9	rexlimdva	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
11	1 10	syl5	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
12	11	impl	⊢ ( ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) )
13	12	ralrimiva	⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) → ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) )
14	13	anim2i	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ) → ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
15		3anass	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ) )
16		dffo3	⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
17	14 15 16	3imtr4i	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) → 𝐹 : 𝐵 –onto→ 𝐶 )