![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ontr1 | Structured version Visualization version GIF version |
Description: Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
ontr1 | ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 6366 | . 2 ⊢ (𝐶 ∈ On → Ord 𝐶) | |
2 | ordtr1 6399 | . 2 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 Ord word 6355 Oncon0 6356 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-v 3477 df-in 3953 df-ss 3963 df-uni 4905 df-tr 5262 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-ord 6359 df-on 6360 |
This theorem is referenced by: epweon 7749 smoiun 8348 dif20el 8492 oeordi 8575 omabs 8638 omsmolem 8644 naddel12 8687 cofsmo 10251 cfsmolem 10252 inar1 10757 grur1a 10801 nosupno 27173 nosupbnd2lem1 27185 noinfno 27188 noinfbnd2lem1 27200 lrrecpo 27392 addsproplem2 27421 onexoegt 41864 oneltr 41876 oaun3lem1 41995 nadd2rabtr 42005 naddsuc2 42014 naddwordnexlem0 42018 oawordex3 42022 naddwordnexlem4 42023 |
Copyright terms: Public domain | W3C validator |