| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ordtr | Structured version Visualization version GIF version | ||
| Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
| Ref | Expression |
|---|---|
| ordtr | ⊢ (Ord 𝐴 → Tr 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ord 6387 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (Ord 𝐴 → Tr 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Tr wtr 5259 E cep 5583 We wwe 5636 Ord word 6383 |
| 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-ord 6387 |
| This theorem is referenced by: ordelss 6400 ordn2lp 6404 ordelord 6406 tz7.7 6410 ordelssne 6411 ordin 6414 ordtr1 6427 orduniss 6481 ontr 6493 dford5 7804 ordsuci 7828 ordunisuc 7852 limsuc 7870 trom 7896 dfrecs3 8412 dfrecs3OLD 8413 tz7.44-2 8447 cantnflt 9712 cantnfp1lem3 9720 cantnflem1b 9726 cantnflem1 9729 cnfcom 9740 axdc3lem2 10491 inar1 10815 efgmnvl 19732 bnj967 34959 dford3 43040 limsuc2 43053 ordsssucim 43415 ordelordALT 44557 onfrALTlem2 44566 ordelordALTVD 44887 onfrALTlem2VD 44909 iunord 49195 |
| Copyright terms: Public domain | W3C validator |