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 )