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	$$⊢\left(F:B⟶C\wedge G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\to F:B\underset{onto}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		foelrn	$$⊢\left(\left(F\circ G\right):A\underset{onto}{⟶}C\wedge y\in C\right)\to \exists z\in Ay=\left(F\circ G\right)\left(z\right)$$
2		ffvelcdm	$$⊢\left(G:A⟶B\wedge z\in A\right)\to G\left(z\right)\in B$$
3		fvco3	$$⊢\left(G:A⟶B\wedge z\in A\right)\to \left(F\circ G\right)\left(z\right)=F\left(G\left(z\right)\right)$$
4		fveq2	$$⊢x=G\left(z\right)\to F\left(x\right)=F\left(G\left(z\right)\right)$$
5	4	rspceeqv	$$⊢\left(G\left(z\right)\in B\wedge \left(F\circ G\right)\left(z\right)=F\left(G\left(z\right)\right)\right)\to \exists x\in B\left(F\circ G\right)\left(z\right)=F\left(x\right)$$
6	2 3 5	syl2anc	$$⊢\left(G:A⟶B\wedge z\in A\right)\to \exists x\in B\left(F\circ G\right)\left(z\right)=F\left(x\right)$$
7		eqeq1	$$⊢y=\left(F\circ G\right)\left(z\right)\to \left(y=F\left(x\right)\leftrightarrow \left(F\circ G\right)\left(z\right)=F\left(x\right)\right)$$
8	7	rexbidv	$$⊢y=\left(F\circ G\right)\left(z\right)\to \left(\exists x\in By=F\left(x\right)\leftrightarrow \exists x\in B\left(F\circ G\right)\left(z\right)=F\left(x\right)\right)$$
9	6 8	syl5ibrcom	$$⊢\left(G:A⟶B\wedge z\in A\right)\to \left(y=\left(F\circ G\right)\left(z\right)\to \exists x\in By=F\left(x\right)\right)$$
10	9	rexlimdva	$$⊢G:A⟶B\to \left(\exists z\in Ay=\left(F\circ G\right)\left(z\right)\to \exists x\in By=F\left(x\right)\right)$$
11	1 10	syl5	$$⊢G:A⟶B\to \left(\left(\left(F\circ G\right):A\underset{onto}{⟶}C\wedge y\in C\right)\to \exists x\in By=F\left(x\right)\right)$$
12	11	impl	$$⊢\left(\left(G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\wedge y\in C\right)\to \exists x\in By=F\left(x\right)$$
13	12	ralrimiva	$$⊢\left(G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\to \forall y\in C\exists x\in By=F\left(x\right)$$
14	13	anim2i	$$⊢\left(F:B⟶C\wedge \left(G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\right)\to \left(F:B⟶C\wedge \forall y\in C\exists x\in By=F\left(x\right)\right)$$
15		3anass	$$⊢\left(F:B⟶C\wedge G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\leftrightarrow \left(F:B⟶C\wedge \left(G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\right)$$
16		dffo3	$$⊢F:B\underset{onto}{⟶}C\leftrightarrow \left(F:B⟶C\wedge \forall y\in C\exists x\in By=F\left(x\right)\right)$$
17	14 15 16	3imtr4i	$$⊢\left(F:B⟶C\wedge G:A⟶B\wedge \left(F\circ G\right):A\underset{onto}{⟶}C\right)\to F:B\underset{onto}{⟶}C$$