| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > trssord | Structured version Visualization version GIF version | ||
| Description: A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
| Ref | Expression |
|---|---|
| trssord | ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wess 5671 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( E We 𝐵 → E We 𝐴)) | |
| 2 | ordwe 6397 | . . . . 5 ⊢ (Ord 𝐵 → E We 𝐵) | |
| 3 | 1, 2 | impel 505 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → E We 𝐴) |
| 4 | 3 | anim2i 617 | . . 3 ⊢ ((Tr 𝐴 ∧ (𝐴 ⊆ 𝐵 ∧ Ord 𝐵)) → (Tr 𝐴 ∧ E We 𝐴)) |
| 5 | 4 | 3impb 1115 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → (Tr 𝐴 ∧ E We 𝐴)) |
| 6 | df-ord 6387 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
| 7 | 5, 6 | sylibr 234 | 1 ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ⊆ wss 3951 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 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-ral 3062 df-ss 3968 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 |
| This theorem is referenced by: ordin 6414 ssorduni 7799 ordsuci 7828 sucexeloniOLD 7830 suceloniOLD 7832 ordom 7897 ordtypelem2 9559 hartogs 9584 card2on 9594 tskwe 9990 ondomon 10603 dford3lem2 43039 dford3 43040 iunord 49195 |
| Copyright terms: Public domain | W3C validator |