This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovord

Description: Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996)

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

Proof

Step	Hyp	Ref	Expression
1		caovord.1	⊢ 𝐴 ∈ V
2		caovord.2	⊢ 𝐵 ∈ V
3		caovord.3	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) )
4		oveq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝐹 𝐴 ) = ( 𝐶 𝐹 𝐴 ) )
5		oveq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐵 ) )
6	4 5	breq12d	⊢ ( 𝑧 = 𝐶 → ( ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
7	6	bibi2d	⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝑅 𝐵 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) ↔ ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) )
8		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝑦 ) )
9		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑧 𝐹 𝑥 ) = ( 𝑧 𝐹 𝐴 ) )
10	9	breq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) )
11	8 10	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ↔ ( 𝐴 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ) )
12		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
13		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝑧 𝐹 𝑦 ) = ( 𝑧 𝐹 𝐵 ) )
14	13	breq2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) )
15	12 14	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ↔ ( 𝐴 𝑅 𝐵 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) ) )
16	11 15	sylan9bb	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ↔ ( 𝐴 𝑅 𝐵 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) ) )
17	16	imbi2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑧 ∈ 𝑆 → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ) ↔ ( 𝑧 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) ) ) )
18	1 2 17 3	vtocl2	⊢ ( 𝑧 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝑧 𝐹 𝐴 ) 𝑅 ( 𝑧 𝐹 𝐵 ) ) )
19	7 18	vtoclga	⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )