f1opr

Description: Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010)

		Ref	Expression
	Assertion	f1opr	$⊢ F : A \times B \underset{1-1}{⟶} C \leftrightarrow (F : A \times B ⟶ C \land \forall r \in A \forall s \in B \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u)))$

Proof

Step	Hyp	Ref	Expression
1		dff13	$⊢ F : A \times B \underset{1-1}{⟶} C \leftrightarrow (F : A \times B ⟶ C \land \forall v \in (A \times B) \forall w \in (A \times B) (F (v) = F (w) \to v = w))$
2		fveq2	$⊢ v = ⟨r, s⟩ \to F (v) = F (⟨r, s⟩)$
3		df-ov	$⊢ r F s = F (⟨r, s⟩)$
4	2 3	eqtr4di	$⊢ v = ⟨r, s⟩ \to F (v) = r F s$
5	4	eqeq1d	$⊢ v = ⟨r, s⟩ \to (F (v) = F (w) \leftrightarrow r F s = F (w))$
6		eqeq1	$⊢ v = ⟨r, s⟩ \to (v = w \leftrightarrow ⟨r, s⟩ = w)$
7	5 6	imbi12d	$⊢ v = ⟨r, s⟩ \to ((F (v) = F (w) \to v = w) \leftrightarrow (r F s = F (w) \to ⟨r, s⟩ = w))$
8	7	ralbidv	$⊢ v = ⟨r, s⟩ \to (\forall w \in (A \times B) (F (v) = F (w) \to v = w) \leftrightarrow \forall w \in (A \times B) (r F s = F (w) \to ⟨r, s⟩ = w))$
9	8	ralxp	$⊢ \forall v \in (A \times B) \forall w \in (A \times B) (F (v) = F (w) \to v = w) \leftrightarrow \forall r \in A \forall s \in B \forall w \in (A \times B) (r F s = F (w) \to ⟨r, s⟩ = w)$
10		fveq2	$⊢ w = ⟨t, u⟩ \to F (w) = F (⟨t, u⟩)$
11		df-ov	$⊢ t F u = F (⟨t, u⟩)$
12	10 11	eqtr4di	$⊢ w = ⟨t, u⟩ \to F (w) = t F u$
13	12	eqeq2d	$⊢ w = ⟨t, u⟩ \to (r F s = F (w) \leftrightarrow r F s = t F u)$
14		eqeq2	$⊢ w = ⟨t, u⟩ \to (⟨r, s⟩ = w \leftrightarrow ⟨r, s⟩ = ⟨t, u⟩)$
15		vex	$⊢ r \in V$
16		vex	$⊢ s \in V$
17	15 16	opth	$⊢ ⟨r, s⟩ = ⟨t, u⟩ \leftrightarrow (r = t \land s = u)$
18	14 17	bitrdi	$⊢ w = ⟨t, u⟩ \to (⟨r, s⟩ = w \leftrightarrow (r = t \land s = u))$
19	13 18	imbi12d	$⊢ w = ⟨t, u⟩ \to ((r F s = F (w) \to ⟨r, s⟩ = w) \leftrightarrow (r F s = t F u \to (r = t \land s = u)))$
20	19	ralxp	$⊢ \forall w \in (A \times B) (r F s = F (w) \to ⟨r, s⟩ = w) \leftrightarrow \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u))$
21	20	2ralbii	$⊢ \forall r \in A \forall s \in B \forall w \in (A \times B) (r F s = F (w) \to ⟨r, s⟩ = w) \leftrightarrow \forall r \in A \forall s \in B \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u))$
22	9 21	bitri	$⊢ \forall v \in (A \times B) \forall w \in (A \times B) (F (v) = F (w) \to v = w) \leftrightarrow \forall r \in A \forall s \in B \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u))$
23	22	anbi2i	$⊢ (F : A \times B ⟶ C \land \forall v \in (A \times B) \forall w \in (A \times B) (F (v) = F (w) \to v = w)) \leftrightarrow (F : A \times B ⟶ C \land \forall r \in A \forall s \in B \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u)))$
24	1 23	bitri	$⊢ F : A \times B \underset{1-1}{⟶} C \leftrightarrow (F : A \times B ⟶ C \land \forall r \in A \forall s \in B \forall t \in A \forall u \in B (r F s = t F u \to (r = t \land s = u)))$

Metamath Proof Explorer

Theorem f1opr

Proof