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 5511 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simprbi 500 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Or wor 5467 Fr wfr 5506 We wwe 5508 |
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 210 df-an 400 df-we 5511 |
This theorem is referenced by: wecmpep 5543 wetrep 5544 wereu 5547 wereu2 5548 weniso 7163 wexp 7897 wfrlem10 8064 ordunifi 8921 ordtypelem7 9140 ordtypelem8 9141 hartogslem1 9158 wofib 9161 wemapso 9167 oemapso 9297 cantnf 9308 ween 9649 cflim2 9877 fin23lem27 9942 zorn2lem1 10110 zorn2lem4 10113 fpwwe2lem11 10255 fpwwe2lem12 10256 fpwwe2 10257 canth4 10261 canthwelem 10264 pwfseqlem4 10276 ltsopi 10502 wzel 33555 wsuccl 33558 wsuclb 33559 on2recsfn 33563 on2recsov 33564 on2ind 33565 on3ind 33566 welb 35631 wepwso 40571 fnwe2lem3 40580 wessf1ornlem 42395 |
Copyright terms: Public domain | W3C validator |