![]() |
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 5944 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
2 | 1 | simplbi 492 | 1 ⊢ (Ord 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Tr wtr 4945 E cep 5224 We wwe 5270 Ord word 5940 |
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 199 df-an 386 df-ord 5944 |
This theorem is referenced by: ordelss 5957 ordn2lp 5961 ordelord 5963 tz7.7 5967 ordelssne 5968 ordin 5971 ordtr1 5984 orduniss 6035 ontrci 6046 ordunisuc 7266 onuninsuci 7274 limsuc 7283 ordom 7308 elnn 7309 omsinds 7318 dfrecs3 7708 tz7.44-2 7742 cantnflt 8819 cantnfp1lem3 8827 cantnflem1b 8833 cantnflem1 8836 cnfcom 8847 axdc3lem2 9561 inar1 9885 efgmnvl 18440 bnj967 31532 dford5 32123 dford3 38376 limsuc2 38392 ordelordALT 39519 onfrALTlem2 39528 ordelordALTVD 39859 onfrALTlem2VD 39881 iunord 43217 |
Copyright terms: Public domain | W3C validator |