Theorem wesn

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

	Ref	Expression
Assertion	wesn	⊢ ( Rel 𝑅 → ( 𝑅 We { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		frsn	⊢ ( Rel 𝑅 → ( 𝑅 Fr { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
2		sosn	⊢ ( Rel 𝑅 → ( 𝑅 Or { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
3	1 2	anbi12d	⊢ ( Rel 𝑅 → ( ( 𝑅 Fr { 𝐴 } ∧ 𝑅 Or { 𝐴 } ) ↔ ( ¬ 𝐴 𝑅 𝐴 ∧ ¬ 𝐴 𝑅 𝐴 ) ) )
4		df-we	⊢ ( 𝑅 We { 𝐴 } ↔ ( 𝑅 Fr { 𝐴 } ∧ 𝑅 Or { 𝐴 } ) )
5		pm4.24	⊢ ( ¬ 𝐴 𝑅 𝐴 ↔ ( ¬ 𝐴 𝑅 𝐴 ∧ ¬ 𝐴 𝑅 𝐴 ) )
6	3 4 5	3bitr4g	⊢ ( Rel 𝑅 → ( 𝑅 We { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )