Metamath Proof Explorer

Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ssorduni $⊢ A ⊆ On → Ord ⁡ ⋃ A$

Proof

Step Hyp Ref Expression
1 eluni2 $⊢ x ∈ ⋃ A ↔ ∃ y ∈ A x ∈ y$
2 ssel $⊢ A ⊆ On → y ∈ A → y ∈ On$
3 onelss $⊢ y ∈ On → x ∈ y → x ⊆ y$
4 2 3 syl6 $⊢ A ⊆ On → y ∈ A → x ∈ y → x ⊆ y$
5 anc2r $⊢ y ∈ A → x ∈ y → x ⊆ y → y ∈ A → x ∈ y → x ⊆ y ∧ y ∈ A$
6 4 5 syl $⊢ A ⊆ On → y ∈ A → x ∈ y → x ⊆ y ∧ y ∈ A$
7 ssuni $⊢ x ⊆ y ∧ y ∈ A → x ⊆ ⋃ A$
8 6 7 syl8 $⊢ A ⊆ On → y ∈ A → x ∈ y → x ⊆ ⋃ A$
9 8 rexlimdv $⊢ A ⊆ On → ∃ y ∈ A x ∈ y → x ⊆ ⋃ A$
10 1 9 syl5bi $⊢ A ⊆ On → x ∈ ⋃ A → x ⊆ ⋃ A$
11 10 ralrimiv $⊢ A ⊆ On → ∀ x ∈ ⋃ A x ⊆ ⋃ A$
12 dftr3 $⊢ Tr ⁡ ⋃ A ↔ ∀ x ∈ ⋃ A x ⊆ ⋃ A$
13 11 12 sylibr $⊢ A ⊆ On → Tr ⁡ ⋃ A$
14 onelon $⊢ y ∈ On ∧ x ∈ y → x ∈ On$
15 14 ex $⊢ y ∈ On → x ∈ y → x ∈ On$
16 2 15 syl6 $⊢ A ⊆ On → y ∈ A → x ∈ y → x ∈ On$
17 16 rexlimdv $⊢ A ⊆ On → ∃ y ∈ A x ∈ y → x ∈ On$
18 1 17 syl5bi $⊢ A ⊆ On → x ∈ ⋃ A → x ∈ On$
19 18 ssrdv $⊢ A ⊆ On → ⋃ A ⊆ On$
20 ordon $⊢ Ord ⁡ On$
21 trssord $⊢ Tr ⁡ ⋃ A ∧ ⋃ A ⊆ On ∧ Ord ⁡ On → Ord ⁡ ⋃ A$
22 21 3exp $⊢ Tr ⁡ ⋃ A → ⋃ A ⊆ On → Ord ⁡ On → Ord ⁡ ⋃ A$
23 20 22 mpii $⊢ Tr ⁡ ⋃ A → ⋃ A ⊆ On → Ord ⁡ ⋃ A$
24 13 19 23 sylc $⊢ A ⊆ On → Ord ⁡ ⋃ A$