Metamath Proof Explorer

Theorem ordsssuc2

Description: An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ordsssuc2 ⊢ Ord ⁡ A ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B

Proof

Step Hyp Ref Expression
1 elong ⊢ A ∈ V → A ∈ On ↔ Ord ⁡ A
2 1 biimprd ⊢ A ∈ V → Ord ⁡ A → A ∈ On
3 2 anim1d ⊢ A ∈ V → Ord ⁡ A ∧ B ∈ On → A ∈ On ∧ B ∈ On
4 onsssuc ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B
5 3 4 syl6 ⊢ A ∈ V → Ord ⁡ A ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B
6 annim ⊢ B ∈ On ∧ ¬ A ∈ V ↔ ¬ B ∈ On → A ∈ V
7 ssexg ⊢ A ⊆ B ∧ B ∈ On → A ∈ V
8 7 ex ⊢ A ⊆ B → B ∈ On → A ∈ V
9 elex ⊢ A ∈ suc ⁡ B → A ∈ V
10 9 a1d ⊢ A ∈ suc ⁡ B → B ∈ On → A ∈ V
11 8 10 pm5.21ni ⊢ ¬ B ∈ On → A ∈ V → A ⊆ B ↔ A ∈ suc ⁡ B
12 6 11 sylbi ⊢ B ∈ On ∧ ¬ A ∈ V → A ⊆ B ↔ A ∈ suc ⁡ B
13 12 expcom ⊢ ¬ A ∈ V → B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B
14 13 adantld ⊢ ¬ A ∈ V → Ord ⁡ A ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B
15 5 14 pm2.61i ⊢ Ord ⁡ A ∧ B ∈ On → A ⊆ B ↔ A ∈ suc ⁡ B