# Metamath Proof Explorer

## Theorem ordtr2

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ordtr2 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{C}\right)\to \left(\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\in {C}\right)$

### Proof

Step Hyp Ref Expression
1 ordelord ${⊢}\left(\mathrm{Ord}{C}\wedge {B}\in {C}\right)\to \mathrm{Ord}{B}$
2 1 ex ${⊢}\mathrm{Ord}{C}\to \left({B}\in {C}\to \mathrm{Ord}{B}\right)$
3 2 ancld ${⊢}\mathrm{Ord}{C}\to \left({B}\in {C}\to \left({B}\in {C}\wedge \mathrm{Ord}{B}\right)\right)$
4 3 anc2li ${⊢}\mathrm{Ord}{C}\to \left({B}\in {C}\to \left(\mathrm{Ord}{C}\wedge \left({B}\in {C}\wedge \mathrm{Ord}{B}\right)\right)\right)$
5 ordelpss ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({B}\in {C}↔{B}\subset {C}\right)$
6 sspsstr ${⊢}\left({A}\subseteq {B}\wedge {B}\subset {C}\right)\to {A}\subset {C}$
7 6 expcom ${⊢}{B}\subset {C}\to \left({A}\subseteq {B}\to {A}\subset {C}\right)$
8 5 7 syl6bi ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({B}\in {C}\to \left({A}\subseteq {B}\to {A}\subset {C}\right)\right)$
9 8 expcom ${⊢}\mathrm{Ord}{C}\to \left(\mathrm{Ord}{B}\to \left({B}\in {C}\to \left({A}\subseteq {B}\to {A}\subset {C}\right)\right)\right)$
10 9 com23 ${⊢}\mathrm{Ord}{C}\to \left({B}\in {C}\to \left(\mathrm{Ord}{B}\to \left({A}\subseteq {B}\to {A}\subset {C}\right)\right)\right)$
11 10 imp32 ${⊢}\left(\mathrm{Ord}{C}\wedge \left({B}\in {C}\wedge \mathrm{Ord}{B}\right)\right)\to \left({A}\subseteq {B}\to {A}\subset {C}\right)$
12 11 com12 ${⊢}{A}\subseteq {B}\to \left(\left(\mathrm{Ord}{C}\wedge \left({B}\in {C}\wedge \mathrm{Ord}{B}\right)\right)\to {A}\subset {C}\right)$
13 4 12 syl9 ${⊢}\mathrm{Ord}{C}\to \left({A}\subseteq {B}\to \left({B}\in {C}\to {A}\subset {C}\right)\right)$
14 13 impd ${⊢}\mathrm{Ord}{C}\to \left(\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\subset {C}\right)$
15 14 adantl ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{C}\right)\to \left(\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\subset {C}\right)$
16 ordelpss ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{C}\right)\to \left({A}\in {C}↔{A}\subset {C}\right)$
17 15 16 sylibrd ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{C}\right)\to \left(\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\in {C}\right)$