|   | 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 6393 | . 2 ⊢ (𝐶 ∈ On → Ord 𝐶) | |
| 2 | ordtr1 6426 | . 2 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 Ord word 6382 Oncon0 6383 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-v 3481 df-ss 3967 df-uni 4907 df-tr 5259 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-ord 6386 df-on 6387 | 
| This theorem is referenced by: epweon 7796 smoiun 8402 dif20el 8544 oeordi 8626 omabs 8690 omsmolem 8696 naddel12 8739 naddsuc2 8740 cofsmo 10310 cfsmolem 10311 inar1 10816 grur1a 10860 nosupno 27749 nosupbnd2lem1 27761 noinfno 27764 noinfbnd2lem1 27776 lrrecpo 27975 addsproplem2 28004 onexoegt 43261 oneltr 43273 oaun3lem1 43392 nadd2rabtr 43402 naddwordnexlem0 43414 oawordex3 43418 naddwordnexlem4 43419 | 
| Copyright terms: Public domain | W3C validator |