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

Metamath Proof Explorer

Theorem sosn

Description: Strict ordering on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Assertion sosn ⊢ Rel ⁡ R → R Or A ↔ ¬ A R A

Proof

Step Hyp Ref Expression
1 elsni ⊢ x ∈ A → x = A
2 elsni ⊢ y ∈ A → y = A
3 2 eqcomd ⊢ y ∈ A → A = y
4 1 3 sylan9eq ⊢ x ∈ A ∧ y ∈ A → x = y
5 4 3mix2d ⊢ x ∈ A ∧ y ∈ A → x R y ∨ x = y ∨ y R x
6 5 rgen2 ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
7 df-so ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
8 6 7 mpbiran2 ⊢ R Or A ↔ R Po A
9 posn ⊢ Rel ⁡ R → R Po A ↔ ¬ A R A
10 8 9 bitrid ⊢ Rel ⁡ R → R Or A ↔ ¬ A R A