Theorem caovord2

Description: Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996)

	Ref	Expression
Hypotheses	caovord.1	⊢ 𝐴 ∈ V
	caovord.2	⊢ 𝐵 ∈ V
	caovord.3	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) )
	caovord2.3	⊢ 𝐶 ∈ V
	caovord2.com	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
Assertion	caovord2	⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐶 ) 𝑅 ( 𝐵 𝐹 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		caovord.1	⊢ 𝐴 ∈ V
2		caovord.2	⊢ 𝐵 ∈ V
3		caovord.3	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) )
4		caovord2.3	⊢ 𝐶 ∈ V
5		caovord2.com	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
6	1 2 3	caovord	⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
7	4 1 5	caovcom	⊢ ( 𝐶 𝐹 𝐴 ) = ( 𝐴 𝐹 𝐶 )
8	4 2 5	caovcom	⊢ ( 𝐶 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐶 )
9	7 8	breq12i	⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ↔ ( 𝐴 𝐹 𝐶 ) 𝑅 ( 𝐵 𝐹 𝐶 ) )
10	6 9	bitrdi	⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐶 ) 𝑅 ( 𝐵 𝐹 𝐶 ) ) )