Metamath Proof Explorer

Theorem iunord

Description: The indexed union of a collection of ordinal numbers B ( x ) is ordinal. This proof is based on the proof of ssorduni , but does not use it directly, since ssorduni does not work when B is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019)

Ref Expression
Assertion iunord ⊢ ∀ x ∈ A Ord ⁡ B → Ord ⁡ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 ordtr ⊢ Ord ⁡ B → Tr ⁡ B
2 1 ralimi ⊢ ∀ x ∈ A Ord ⁡ B → ∀ x ∈ A Tr ⁡ B
3 triun ⊢ ∀ x ∈ A Tr ⁡ B → Tr ⁡ ⋃ x ∈ A B
4 2 3 syl ⊢ ∀ x ∈ A Ord ⁡ B → Tr ⁡ ⋃ x ∈ A B
5 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
6 nfra1 ⊢ Ⅎ x ∀ x ∈ A Ord ⁡ B
7 nfv ⊢ Ⅎ x y ∈ On
8 rsp ⊢ ∀ x ∈ A Ord ⁡ B → x ∈ A → Ord ⁡ B
9 ordelon ⊢ Ord ⁡ B ∧ y ∈ B → y ∈ On
10 9 ex ⊢ Ord ⁡ B → y ∈ B → y ∈ On
11 8 10 syl6 ⊢ ∀ x ∈ A Ord ⁡ B → x ∈ A → y ∈ B → y ∈ On
12 6 7 11 rexlimd ⊢ ∀ x ∈ A Ord ⁡ B → ∃ x ∈ A y ∈ B → y ∈ On
13 5 12 syl5bi ⊢ ∀ x ∈ A Ord ⁡ B → y ∈ ⋃ x ∈ A B → y ∈ On
14 13 ssrdv ⊢ ∀ x ∈ A Ord ⁡ B → ⋃ x ∈ A B ⊆ On
15 ordon ⊢ Ord ⁡ On
16 trssord ⊢ Tr ⁡ ⋃ x ∈ A B ∧ ⋃ x ∈ A B ⊆ On ∧ Ord ⁡ On → Ord ⁡ ⋃ x ∈ A B
17 16 3exp ⊢ Tr ⁡ ⋃ x ∈ A B → ⋃ x ∈ A B ⊆ On → Ord ⁡ On → Ord ⁡ ⋃ x ∈ A B
18 15 17 mpii ⊢ Tr ⁡ ⋃ x ∈ A B → ⋃ x ∈ A B ⊆ On → Ord ⁡ ⋃ x ∈ A B
19 4 14 18 sylc ⊢ ∀ x ∈ A Ord ⁡ B → Ord ⁡ ⋃ x ∈ A B