Theorem rankuniss

Description: Upper bound of the rank of a union. Part of Exercise 30 of Enderton p. 207. (Contributed by NM, 30-Nov-2003)

	Ref	Expression
Hypothesis	rankr1b.1	⊢ 𝐴 ∈ V
Assertion	rankuniss	⊢ ( rank ‘ ∪ 𝐴 ) ⊆ ( rank ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	⊢ 𝐴 ∈ V
2		rankuni	⊢ ( rank ‘ ∪ 𝐴 ) = ∪ ( rank ‘ 𝐴 )
3		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
4	3	onordi	⊢ Ord ( rank ‘ 𝐴 )
5		orduniss	⊢ ( Ord ( rank ‘ 𝐴 ) → ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) )
6	4 5	ax-mp	⊢ ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )
7	2 6	eqsstri	⊢ ( rank ‘ ∪ 𝐴 ) ⊆ ( rank ‘ 𝐴 )