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 6187 | . 2 ⊢ (Ord 𝐶 → Tr 𝐶) | |
2 | trel 5144 | . 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2114 Tr wtr 5137 Ord word 6172 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3401 df-in 3851 df-ss 3861 df-uni 4798 df-tr 5138 df-ord 6176 |
This theorem is referenced by: ontr1 6219 dfsmo2 8016 smores2 8023 smoel 8029 smogt 8036 ordiso2 9055 r1ordg 9283 r1pwss 9289 r1val1 9291 rankr1ai 9303 rankval3b 9331 rankonidlem 9333 onssr1 9336 cofsmo 9772 fpwwe2lem8 10141 bnj1098 32337 bnj594 32466 nosepssdm 33535 |
Copyright terms: Public domain | W3C validator |