| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ordtr1 | Structured version Visualization version GIF version | ||
| Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
| Ref | Expression |
|---|---|
| ordtr1 | ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ordtr 6398 | . 2 ⊢ (Ord 𝐶 → Tr 𝐶) | |
| 2 | trel 5268 | . 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Tr wtr 5259 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 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 df-tr 5260 df-ord 6387 |
| This theorem is referenced by: ontr1 6430 dfsmo2 8387 smores2 8394 smoel 8400 smogt 8407 ordiso2 9555 r1ordg 9818 r1pwss 9824 r1val1 9826 rankr1ai 9838 rankval3b 9866 rankonidlem 9868 onssr1 9871 cofsmo 10309 fpwwe2lem8 10678 nosepssdm 27731 bnj1098 34797 bnj594 34926 |
| Copyright terms: Public domain | W3C validator |