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 6187 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
2 | 1 | simplbi 498 | 1 ⊢ (Ord 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Tr wtr 5163 E cep 5457 We wwe 5506 Ord word 6183 |
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 208 df-an 397 df-ord 6187 |
This theorem is referenced by: ordelss 6200 ordn2lp 6204 ordelord 6206 tz7.7 6210 ordelssne 6211 ordin 6214 ordtr1 6227 orduniss 6278 ontrci 6289 ordunisuc 7536 onuninsuci 7544 limsuc 7553 ordom 7578 elnn 7579 omsinds 7589 dfrecs3 7998 tz7.44-2 8032 cantnflt 9123 cantnfp1lem3 9131 cantnflem1b 9137 cantnflem1 9140 cnfcom 9151 axdc3lem2 9861 inar1 10185 efgmnvl 18769 bnj967 32116 dford5 32854 dford3 39503 limsuc2 39519 ordelordALT 40748 onfrALTlem2 40757 ordelordALTVD 41078 onfrALTlem2VD 41100 iunord 44707 |
Copyright terms: Public domain | W3C validator |