Theorem f1cofveqaeqALT

Description: Alternate proof of f1cofveqaeq , 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	f1cofveqaeqALT	$$⊢\left(\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\to X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1f	$$⊢G:A\underset{1-1}{⟶}B\to G:A⟶B$$
2		fvco3	$$⊢\left(G:A⟶B\wedge X\in A\right)\to \left(F\circ G\right)\left(X\right)=F\left(G\left(X\right)\right)$$
3	2	adantrr	$$⊢\left(G:A⟶B\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(F\circ G\right)\left(X\right)=F\left(G\left(X\right)\right)$$
4		fvco3	$$⊢\left(G:A⟶B\wedge Y\in A\right)\to \left(F\circ G\right)\left(Y\right)=F\left(G\left(Y\right)\right)$$
5	4	adantrl	$$⊢\left(G:A⟶B\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(F\circ G\right)\left(Y\right)=F\left(G\left(Y\right)\right)$$
6	3 5	eqeq12d	$$⊢\left(G:A⟶B\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\leftrightarrow F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\right)$$
7	6	ex	$$⊢G:A⟶B\to \left(\left(X\in A\wedge Y\in A\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\leftrightarrow F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\right)\right)$$
8	1 7	syl	$$⊢G:A\underset{1-1}{⟶}B\to \left(\left(X\in A\wedge Y\in A\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\leftrightarrow F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\right)\right)$$
9	8	adantl	$$⊢\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\to \left(\left(X\in A\wedge Y\in A\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\leftrightarrow F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\right)\right)$$
10	9	imp	$$⊢\left(\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\leftrightarrow F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\right)$$
11		f1co	$$⊢\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\to \left(F\circ G\right):A\underset{1-1}{⟶}C$$
12		f1veqaeq	$$⊢\left(\left(F\circ G\right):A\underset{1-1}{⟶}C\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\to X=Y\right)$$
13	11 12	sylan	$$⊢\left(\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(\left(F\circ G\right)\left(X\right)=\left(F\circ G\right)\left(Y\right)\to X=Y\right)$$
14	10 13	sylbird	$$⊢\left(\left(F:B\underset{1-1}{⟶}C\wedge G:A\underset{1-1}{⟶}B\right)\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(F\left(G\left(X\right)\right)=F\left(G\left(Y\right)\right)\to X=Y\right)$$