Metamath Proof Explorer
Description: Define the antisymmetric relation predicate. (Read: R is an
antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024)
|
|
Ref |
Expression |
|
Assertion |
df-antisymrel |
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel 𝑅 ) ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
cR |
⊢ 𝑅 |
| 1 |
0
|
wantisymrel |
⊢ AntisymRel 𝑅 |
| 2 |
0
|
ccnv |
⊢ ◡ 𝑅 |
| 3 |
0 2
|
cin |
⊢ ( 𝑅 ∩ ◡ 𝑅 ) |
| 4 |
3
|
wcnvrefrel |
⊢ CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) |
| 5 |
0
|
wrel |
⊢ Rel 𝑅 |
| 6 |
4 5
|
wa |
⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel 𝑅 ) |
| 7 |
1 6
|
wb |
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel 𝑅 ) ) |