![]() |
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 6391 | . . . . 5 ⊢ (Ord 𝐵 → E We 𝐵) | |
3 | 1, 2 | impel 504 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → E We 𝐴) |
4 | 3 | anim2i 615 | . . 3 ⊢ ((Tr 𝐴 ∧ (𝐴 ⊆ 𝐵 ∧ Ord 𝐵)) → (Tr 𝐴 ∧ E We 𝐴)) |
5 | 4 | 3impb 1112 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → (Tr 𝐴 ∧ E We 𝐴)) |
6 | df-ord 6381 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
7 | 5, 6 | sylibr 233 | 1 ⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 ⊆ wss 3947 Tr wtr 5272 E cep 5587 We wwe 5638 Ord word 6377 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-ral 3052 df-ss 3964 df-po 5596 df-so 5597 df-fr 5639 df-we 5641 df-ord 6381 |
This theorem is referenced by: ordin 6408 ssorduni 7789 ordsuci 7819 sucexeloniOLD 7821 suceloniOLD 7823 ordom 7888 ordtypelem2 9564 hartogs 9589 card2on 9599 tskwe 9995 ondomon 10608 dford3lem2 42703 dford3 42704 iunord 48440 |
Copyright terms: Public domain | W3C validator |