Step |
Hyp |
Ref |
Expression |
1 |
|
caovordg.1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝑧 𝐹 𝑥 ) 𝑅 ( 𝑧 𝐹 𝑦 ) ) ) |
2 |
|
caovordd.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑆 ) |
3 |
|
caovordd.3 |
⊢ ( 𝜑 → 𝐵 ∈ 𝑆 ) |
4 |
|
caovordd.4 |
⊢ ( 𝜑 → 𝐶 ∈ 𝑆 ) |
5 |
|
caovord2d.com |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) |
6 |
|
caovord3d.5 |
⊢ ( 𝜑 → 𝐷 ∈ 𝑆 ) |
7 |
|
breq1 |
⊢ ( ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) → ( ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) |
8 |
1 2 4 3 5
|
caovord2d |
⊢ ( 𝜑 → ( 𝐴 𝑅 𝐶 ↔ ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) |
9 |
1 6 3 4
|
caovordd |
⊢ ( 𝜑 → ( 𝐷 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) |
10 |
8 9
|
bibi12d |
⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐶 ↔ 𝐷 𝑅 𝐵 ) ↔ ( ( 𝐴 𝐹 𝐵 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ↔ ( 𝐶 𝐹 𝐷 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) ) |
11 |
7 10
|
syl5ibr |
⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) = ( 𝐶 𝐹 𝐷 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐷 𝑅 𝐵 ) ) ) |