This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Ordinals (continued) ssonuni
Description: The union of a set of ordinal numbers is an ordinal number. Theorem 9 of
Suppes p. 132. Lemma 2.7 of Schloeder p. 4. (Contributed by NM , 1-Nov-2003)
Ref
Expression
Assertion
ssonuni ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
Proof
Step
Hyp
Ref
Expression
1
ssorduni ⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
2
uniexg ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
3
elong ⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) )
4
2 3
syl ⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) )
5
1 4
imbitrrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )