Metamath Proof Explorer

Theorem ordunisssuc

Description: A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordunisssuc ⊢ A ⊆ On ∧ Ord ⁡ B → ⋃ A ⊆ B ↔ A ⊆ suc ⁡ B

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ A ⊆ On ∧ x ∈ A → x ∈ On
2 ordsssuc ⊢ x ∈ On ∧ Ord ⁡ B → x ⊆ B ↔ x ∈ suc ⁡ B
3 1 2 sylan ⊢ A ⊆ On ∧ x ∈ A ∧ Ord ⁡ B → x ⊆ B ↔ x ∈ suc ⁡ B
4 3 an32s ⊢ A ⊆ On ∧ Ord ⁡ B ∧ x ∈ A → x ⊆ B ↔ x ∈ suc ⁡ B
5 4 ralbidva ⊢ A ⊆ On ∧ Ord ⁡ B → ∀ x ∈ A x ⊆ B ↔ ∀ x ∈ A x ∈ suc ⁡ B
6 unissb ⊢ ⋃ A ⊆ B ↔ ∀ x ∈ A x ⊆ B
7 dfss3 ⊢ A ⊆ suc ⁡ B ↔ ∀ x ∈ A x ∈ suc ⁡ B
8 5 6 7 3bitr4g ⊢ A ⊆ On ∧ Ord ⁡ B → ⋃ A ⊆ B ↔ A ⊆ suc ⁡ B