![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordwe | Structured version Visualization version GIF version |
Description: Membership 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 6356 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
2 | 1 | simprbi 497 | 1 ⊢ (Ord 𝐴 → E We 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Tr wtr 5258 E cep 5572 We wwe 5623 Ord word 6352 |
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 397 df-ord 6356 |
This theorem is referenced by: ordfr 6368 trssord 6370 tz7.5 6374 ordelord 6375 tz7.7 6379 oieu 9516 oiid 9518 hartogslem1 9519 oemapso 9659 cantnf 9670 oemapwe 9671 dfac8b 10008 fin23lem27 10305 om2uzoi 13902 ltweuz 13908 wepwso 41554 onfrALTlem3 43074 onfrALTlem3VD 43417 |
Copyright terms: Public domain | W3C validator |