![]() |
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 6400 | . 2 ⊢ (Ord 𝐶 → Tr 𝐶) | |
2 | trel 5274 | . 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2106 Tr wtr 5265 Ord word 6385 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-ss 3980 df-uni 4913 df-tr 5266 df-ord 6389 |
This theorem is referenced by: ontr1 6432 dfsmo2 8386 smores2 8393 smoel 8399 smogt 8406 ordiso2 9553 r1ordg 9816 r1pwss 9822 r1val1 9824 rankr1ai 9836 rankval3b 9864 rankonidlem 9866 onssr1 9869 cofsmo 10307 fpwwe2lem8 10676 nosepssdm 27746 bnj1098 34776 bnj594 34905 |
Copyright terms: Public domain | W3C validator |