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 𝑅 → ( 𝑅 Or { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elsni ⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
2 elsni ⊢ ( 𝑦 ∈ { 𝐴 } → 𝑦 = 𝐴 )
3 2 eqcomd ⊢ ( 𝑦 ∈ { 𝐴 } → 𝐴 = 𝑦 )
4 1 3 sylan9eq ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → 𝑥 = 𝑦 )
5 4 3mix2d ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
6 5 rgen2 ⊢ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 )
7 df-so ⊢ ( 𝑅 Or { 𝐴 } ↔ ( 𝑅 Po { 𝐴 } ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
8 6 7 mpbiran2 ⊢ ( 𝑅 Or { 𝐴 } ↔ 𝑅 Po { 𝐴 } )
9 posn ⊢ ( Rel 𝑅 → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
10 8 9 bitrid ⊢ ( Rel 𝑅 → ( 𝑅 Or { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )