|   | 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 5639 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 Or wor 5591 Fr wfr 5634 We wwe 5636 | 
| 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 207 df-an 396 df-we 5639 | 
| This theorem is referenced by: wecmpep 5677 wetrep 5678 wereu 5681 wereu2 5682 tz6.26 6368 wfi 6371 wfisg 6374 wfis2fg 6377 weniso 7374 wexp 8155 wfrlem10OLD 8358 wfrfun 8372 wfrresex 8373 wfr2a 8374 wfr1 8375 on2recsfn 8705 on2recsov 8706 on2ind 8707 on3ind 8708 ordunifi 9326 ordtypelem7 9564 ordtypelem8 9565 hartogslem1 9582 wofib 9585 wemapso 9591 oemapso 9722 cantnf 9733 ween 10075 cflim2 10303 fin23lem27 10368 zorn2lem1 10536 zorn2lem4 10539 fpwwe2lem11 10681 fpwwe2lem12 10682 fpwwe2 10683 canth4 10687 canthwelem 10690 pwfseqlem4 10702 ltsopi 10928 wzel 35825 wsuccl 35828 wsuclb 35829 weiunfrlem 36465 weiunpo 36466 weiunso 36467 weiunwe 36470 welb 37743 wepwso 43055 fnwe2lem3 43064 onsupuni 43241 oninfint 43248 epsoon 43265 epirron 43266 oneptr 43267 wessf1ornlem 45190 | 
| Copyright terms: Public domain | W3C validator |