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 ‘ 𝐴 ) |
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 ‘ 𝐴 ) |