This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ On )

Proof

Step Hyp Ref Expression
1 dfiun3g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
4 rnexg ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
5 3 4 syl ⊢ ( 𝐴 ∈ 𝑉 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 6 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ On )
8 ssonuni ⊢ ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ On → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ On ) )
9 8 imp ⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ On ) → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ On )
10 5 7 9 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ) → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ On )
11 2 10 eqeltrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ On )