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 6280 | . 2 ⊢ (Ord 𝐶 → Tr 𝐶) | |
2 | trel 5198 | . 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 Tr wtr 5191 Ord word 6265 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 df-uni 4840 df-tr 5192 df-ord 6269 |
This theorem is referenced by: ontr1 6312 dfsmo2 8178 smores2 8185 smoel 8191 smogt 8198 ordiso2 9274 r1ordg 9536 r1pwss 9542 r1val1 9544 rankr1ai 9556 rankval3b 9584 rankonidlem 9586 onssr1 9589 cofsmo 10025 fpwwe2lem8 10394 bnj1098 32763 bnj594 32892 nosepssdm 33889 |
Copyright terms: Public domain | W3C validator |