This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ord ⁡ A ∧ Ord ⁡ C → A ⊆ B ∧ B ∈ C → A ∈ C

Proof

Step Hyp Ref Expression
1 ordelord ⊢ Ord ⁡ C ∧ B ∈ C → Ord ⁡ B
2 1 ex ⊢ Ord ⁡ C → B ∈ C → Ord ⁡ B
3 2 ancld ⊢ Ord ⁡ C → B ∈ C → B ∈ C ∧ Ord ⁡ B
4 3 anc2li ⊢ Ord ⁡ C → B ∈ C → Ord ⁡ C ∧ B ∈ C ∧ Ord ⁡ B
5 ordelpss ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ∈ C ↔ B ⊂ C
6 sspsstr ⊢ A ⊆ B ∧ B ⊂ C → A ⊂ C
7 6 expcom ⊢ B ⊂ C → A ⊆ B → A ⊂ C
8 5 7 biimtrdi ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ∈ C → A ⊆ B → A ⊂ C
9 8 expcom ⊢ Ord ⁡ C → Ord ⁡ B → B ∈ C → A ⊆ B → A ⊂ C
10 9 com23 ⊢ Ord ⁡ C → B ∈ C → Ord ⁡ B → A ⊆ B → A ⊂ C
11 10 imp32 ⊢ Ord ⁡ C ∧ B ∈ C ∧ Ord ⁡ B → A ⊆ B → A ⊂ C
12 11 com12 ⊢ A ⊆ B → Ord ⁡ C ∧ B ∈ C ∧ Ord ⁡ B → A ⊂ C
13 4 12 syl9 ⊢ Ord ⁡ C → A ⊆ B → B ∈ C → A ⊂ C
14 13 impd ⊢ Ord ⁡ C → A ⊆ B ∧ B ∈ C → A ⊂ C
15 14 adantl ⊢ Ord ⁡ A ∧ Ord ⁡ C → A ⊆ B ∧ B ∈ C → A ⊂ C
16 ordelpss ⊢ Ord ⁡ A ∧ Ord ⁡ C → A ∈ C ↔ A ⊂ C
17 15 16 sylibrd ⊢ Ord ⁡ A ∧ Ord ⁡ C → A ⊆ B ∧ B ∈ C → A ∈ C