Metamath Proof Explorer

Theorem iunon

Description: The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion iunon ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ On → ⋃ x ∈ A B ∈ On

Proof

Step Hyp Ref Expression
1 dfiun3g ⊢ ∀ x ∈ A B ∈ On → ⋃ x ∈ A B = ⋃ ran ⁡ x ∈ A ⟼ B
2 1 adantl ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ On → ⋃ x ∈ A B = ⋃ ran ⁡ x ∈ A ⟼ B
3 mptexg ⊢ A ∈ V → x ∈ A ⟼ B ∈ V
4 rnexg ⊢ x ∈ A ⟼ B ∈ V → ran ⁡ x ∈ A ⟼ B ∈ V
5 3 4 syl ⊢ A ∈ V → ran ⁡ x ∈ A ⟼ B ∈ V
6 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
7 6 rnmptss ⊢ ∀ x ∈ A B ∈ On → ran ⁡ x ∈ A ⟼ B ⊆ On
8 ssonuni ⊢ ran ⁡ x ∈ A ⟼ B ∈ V → ran ⁡ x ∈ A ⟼ B ⊆ On → ⋃ ran ⁡ x ∈ A ⟼ B ∈ On
9 8 imp ⊢ ran ⁡ x ∈ A ⟼ B ∈ V ∧ ran ⁡ x ∈ A ⟼ B ⊆ On → ⋃ ran ⁡ x ∈ A ⟼ B ∈ On
10 5 7 9 syl2an ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ On → ⋃ ran ⁡ x ∈ A ⟼ B ∈ On
11 2 10 eqeltrd ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ On → ⋃ x ∈ A B ∈ On