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