Theorem f1ocpbl

Description: An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypothesis	f1ocpbl.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}X$$
Assertion	f1ocpbl	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in V\right)\wedge \left(C\in V\wedge D\in V\right)\right)\to \left(\left(F\left(A\right)=F\left(C\right)\wedge F\left(B\right)=F\left(D\right)\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(C\underset{\dot{}}{+}D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1ocpbl.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}X$$
2	1	f1ocpbllem	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in V\right)\wedge \left(C\in V\wedge D\in V\right)\right)\to \left(\left(F\left(A\right)=F\left(C\right)\wedge F\left(B\right)=F\left(D\right)\right)\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
3		oveq12	$$⊢\left(A=C\wedge B=D\right)\to A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D$$
4	3	fveq2d	$$⊢\left(A=C\wedge B=D\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(C\underset{\dot{}}{+}D\right)$$
5	2 4	biimtrdi	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in V\right)\wedge \left(C\in V\wedge D\in V\right)\right)\to \left(\left(F\left(A\right)=F\left(C\right)\wedge F\left(B\right)=F\left(D\right)\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(C\underset{\dot{}}{+}D\right)\right)$$