![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > weso | Structured version Visualization version GIF version |
Description: A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.) |
Ref | Expression |
---|---|
weso | ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-we 5368 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simprbi 489 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Or wor 5325 Fr wfr 5363 We wwe 5365 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 df-an 388 df-we 5368 |
This theorem is referenced by: wecmpep 5399 wetrep 5400 wereu 5403 wereu2 5404 weniso 6930 wexp 7629 wfrlem10 7768 ordunifi 8563 ordtypelem7 8783 ordtypelem8 8784 hartogslem1 8801 wofib 8804 wemapso 8810 oemapso 8939 cantnf 8950 ween 9255 cflim2 9483 fin23lem27 9548 zorn2lem1 9716 zorn2lem4 9719 fpwwe2lem12 9861 fpwwe2lem13 9862 fpwwe2 9863 canth4 9867 canthwelem 9870 pwfseqlem4 9882 ltsopi 10108 wzel 32629 wsuccl 32632 wsuclb 32633 welb 34450 wepwso 39036 fnwe2lem3 39045 wessf1ornlem 40867 |
Copyright terms: Public domain | W3C validator |