![]() |
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 5631 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simprbi 495 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Or wor 5585 Fr wfr 5626 We wwe 5628 |
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 206 df-an 395 df-we 5631 |
This theorem is referenced by: wecmpep 5666 wetrep 5667 wereu 5670 wereu2 5671 tz6.26 6352 wfi 6355 wfisg 6358 wfis2fg 6361 weniso 7358 wexp 8136 wfrlem10OLD 8340 wfrfun 8354 wfrresex 8355 wfr2a 8356 wfr1 8357 on2recsfn 8689 on2recsov 8690 on2ind 8691 on3ind 8692 ordunifi 9320 ordtypelem7 9560 ordtypelem8 9561 hartogslem1 9578 wofib 9581 wemapso 9587 oemapso 9718 cantnf 9729 ween 10071 cflim2 10297 fin23lem27 10362 zorn2lem1 10530 zorn2lem4 10533 fpwwe2lem11 10675 fpwwe2lem12 10676 fpwwe2 10677 canth4 10681 canthwelem 10684 pwfseqlem4 10696 ltsopi 10922 wzel 35661 wsuccl 35664 wsuclb 35665 welb 37450 wepwso 42741 fnwe2lem3 42750 onsupuni 42931 oninfint 42938 epsoon 42955 epirron 42956 oneptr 42957 wessf1ornlem 44828 |
Copyright terms: Public domain | W3C validator |