Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ordwe | Structured version Visualization version GIF version |
Description: Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
ordwe | ⊢ (Ord 𝐴 → E We 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ord 5643 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
2 | 1 | simprbi 479 | 1 ⊢ (Ord 𝐴 → E We 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Tr wtr 4680 E cep 4947 We wwe 4996 Ord word 5639 |
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 196 df-an 385 df-ord 5643 |
This theorem is referenced by: ordfr 5655 trssord 5657 tz7.5 5661 ordelord 5662 tz7.7 5666 epweon 6875 oieu 8327 oiid 8329 hartogslem1 8330 oemapso 8462 cantnf 8473 oemapwe 8474 dfac8b 8737 fin23lem27 9033 om2uzoi 12616 ltweuz 12622 wepwso 36631 onfrALTlem3 37780 onfrALTlem3VD 38145 |
Copyright terms: Public domain | W3C validator |