Metamath Proof Explorer


Theorem wesn

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

Ref Expression
Assertion wesn RelRRWeA¬ARA

Proof

Step Hyp Ref Expression
1 frsn RelRRFrA¬ARA
2 sosn RelRROrA¬ARA
3 1 2 anbi12d RelRRFrAROrA¬ARA¬ARA
4 df-we RWeARFrAROrA
5 pm4.24 ¬ARA¬ARA¬ARA
6 3 4 5 3bitr4g RelRRWeA¬ARA