caovordig

Description: Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014)

		Ref	Expression
	Hypothesis	caovordig.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \to (z F x) R (z F y))$
	Assertion	caovordig	$⊢ (φ \land (A \in S \land B \in S \land C \in S)) \to (A R B \to (C F A) R (C F B))$

Step	Hyp	Ref	Expression
1		caovordig.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \to (z F x) R (z F y))$
2	1	ralrimivvva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S (x R y \to (z F x) R (z F y))$
3		breq1	$⊢ x = A \to (x R y \leftrightarrow A R y)$
4		oveq2	$⊢ x = A \to z F x = z F A$
5	4	breq1d	$⊢ x = A \to ((z F x) R (z F y) \leftrightarrow (z F A) R (z F y))$
6	3 5	imbi12d	$⊢ x = A \to ((x R y \to (z F x) R (z F y)) \leftrightarrow (A R y \to (z F A) R (z F y)))$
7		breq2	$⊢ y = B \to (A R y \leftrightarrow A R B)$
8		oveq2	$⊢ y = B \to z F y = z F B$
9	8	breq2d	$⊢ y = B \to ((z F A) R (z F y) \leftrightarrow (z F A) R (z F B))$
10	7 9	imbi12d	$⊢ y = B \to ((A R y \to (z F A) R (z F y)) \leftrightarrow (A R B \to (z F A) R (z F B)))$
11		oveq1	$⊢ z = C \to z F A = C F A$
12		oveq1	$⊢ z = C \to z F B = C F B$
13	11 12	breq12d	$⊢ z = C \to ((z F A) R (z F B) \leftrightarrow (C F A) R (C F B))$
14	13	imbi2d	$⊢ z = C \to ((A R B \to (z F A) R (z F B)) \leftrightarrow (A R B \to (C F A) R (C F B)))$
15	6 10 14	rspc3v	$⊢ (A \in S \land B \in S \land C \in S) \to (\forall x \in S \forall y \in S \forall z \in S (x R y \to (z F x) R (z F y)) \to (A R B \to (C F A) R (C F B)))$
16	2 15	mpan9	$⊢ (φ \land (A \in S \land B \in S \land C \in S)) \to (A R B \to (C F A) R (C F B))$

Metamath Proof Explorer