Theorem caovord3

Description: Ordering law. (Contributed by NM, 29-Feb-1996)

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

Proof

Step	Hyp	Ref	Expression
1		caovord.1	⊢ 𝐴 ∈ V
2		caovord.2	⊢ 𝐵 ∈ V
3		caovord.3	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) )
4		caovord2.3	⊢ 𝐶 ∈ V
5		caovord2.com	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
6		caovord3.4	⊢ 𝐷 ∈ V
7	1 4 3 2 5	caovord2	⊢ ( 𝐵 ∈ 𝑆 → ( 𝐴 𝑅 𝐶 ↔ ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
8	7	adantr	⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 𝑅 𝐶 ↔ ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
9		breq1	⊢ ( ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) → ( ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
10	8 9	sylan9bb	⊢ ( ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) ) → ( 𝐴 𝑅 𝐶 ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
11	6 2 3	caovord	⊢ ( 𝐶 ∈ 𝑆 → ( 𝐷 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
12	11	ad2antlr	⊢ ( ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) ) → ( 𝐷 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
13	10 12	bitr4d	⊢ ( ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) ) → ( 𝐴 𝑅 𝐶 ↔ 𝐷 𝑅 𝐵 ) )