Metamath Proof Explorer

Theorem ordsucsssuc

Description: The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003)

Ref Expression
Assertion ordsucsssuc ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ suc ⁡ A ⊆ suc ⁡ B

Proof

Step Hyp Ref Expression
1 ordsucelsuc ⊢ Ord ⁡ A → B ∈ A ↔ suc ⁡ B ∈ suc ⁡ A
2 1 notbid ⊢ Ord ⁡ A → ¬ B ∈ A ↔ ¬ suc ⁡ B ∈ suc ⁡ A
3 2 adantr ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ B ∈ A ↔ ¬ suc ⁡ B ∈ suc ⁡ A
4 ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A
5 ordsuc ⊢ Ord ⁡ A ↔ Ord ⁡ suc ⁡ A
6 ordsuc ⊢ Ord ⁡ B ↔ Ord ⁡ suc ⁡ B
7 ordtri1 ⊢ Ord ⁡ suc ⁡ A ∧ Ord ⁡ suc ⁡ B → suc ⁡ A ⊆ suc ⁡ B ↔ ¬ suc ⁡ B ∈ suc ⁡ A
8 5 6 7 syl2anb ⊢ Ord ⁡ A ∧ Ord ⁡ B → suc ⁡ A ⊆ suc ⁡ B ↔ ¬ suc ⁡ B ∈ suc ⁡ A
9 3 4 8 3bitr4d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ suc ⁡ A ⊆ suc ⁡ B