Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 . (Contributed by NM, 3-Apr-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | df-we | |- ( R We A <-> ( R Fr A /\ R Or A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cR | |- R |
|
1 | cA | |- A |
|
2 | 1 0 | wwe | |- R We A |
3 | 1 0 | wfr | |- R Fr A |
4 | 1 0 | wor | |- R Or A |
5 | 3 4 | wa | |- ( R Fr A /\ R Or A ) |
6 | 2 5 | wb | |- ( R We A <-> ( R Fr A /\ R Or A ) ) |