Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | sonr | ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sopo | ⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 ) | |
2 | poirr | ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 ) | |
3 | 1 2 | sylan | ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 ) |