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