Metamath Proof Explorer

Theorem ordsucss

Description: The successor of an element of an ordinal class is a subset of it. Lemma 1.14 of Schloeder p. 2. (Contributed by NM, 21-Jun-1998)

Ref Expression
Assertion ordsucss ⊢Ord⁡B→A∈B→suc⁡A⊆B

Proof

Step Hyp Ref Expression
1 ordelord ⊢Ord⁡B∧A∈B→Ord⁡A
2 ordnbtwn ⊢Ord⁡A→¬A∈B∧B∈suc⁡A
3 imnan ⊢A∈B→¬B∈suc⁡A↔¬A∈B∧B∈suc⁡A
4 2 3 sylibr ⊢Ord⁡A→A∈B→¬B∈suc⁡A
5 4 adantr ⊢Ord⁡A∧Ord⁡B→A∈B→¬B∈suc⁡A
6 ordsuc ⊢Ord⁡A↔Ord⁡suc⁡A
7 ordtri1 ⊢Ord⁡suc⁡A∧Ord⁡B→suc⁡A⊆B↔¬B∈suc⁡A
8 6 7 sylanb ⊢Ord⁡A∧Ord⁡B→suc⁡A⊆B↔¬B∈suc⁡A
9 5 8 sylibrd ⊢Ord⁡A∧Ord⁡B→A∈B→suc⁡A⊆B
10 1 9 sylan ⊢Ord⁡B∧A∈B∧Ord⁡B→A∈B→suc⁡A⊆B
11 10 exp31 ⊢Ord⁡B→A∈B→Ord⁡B→A∈B→suc⁡A⊆B
12 11 pm2.43b ⊢A∈B→Ord⁡B→A∈B→suc⁡A⊆B
13 12 pm2.43b ⊢Ord⁡B→A∈B→suc⁡A⊆B