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