# Metamath Proof Explorer

## Theorem rankxpl

Description: A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypotheses rankxpl.1 ${⊢}{A}\in \mathrm{V}$
rankxpl.2 ${⊢}{B}\in \mathrm{V}$
Assertion rankxpl ${⊢}{A}×{B}\ne \varnothing \to \mathrm{rank}\left({A}\cup {B}\right)\subseteq \mathrm{rank}\left({A}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 rankxpl.1 ${⊢}{A}\in \mathrm{V}$
2 rankxpl.2 ${⊢}{B}\in \mathrm{V}$
3 unixp ${⊢}{A}×{B}\ne \varnothing \to \bigcup \bigcup \left({A}×{B}\right)={A}\cup {B}$
4 3 fveq2d ${⊢}{A}×{B}\ne \varnothing \to \mathrm{rank}\left(\bigcup \bigcup \left({A}×{B}\right)\right)=\mathrm{rank}\left({A}\cup {B}\right)$
5 1 2 xpex ${⊢}{A}×{B}\in \mathrm{V}$
6 5 uniex ${⊢}\bigcup \left({A}×{B}\right)\in \mathrm{V}$
7 6 rankuniss ${⊢}\mathrm{rank}\left(\bigcup \bigcup \left({A}×{B}\right)\right)\subseteq \mathrm{rank}\left(\bigcup \left({A}×{B}\right)\right)$
8 5 rankuniss ${⊢}\mathrm{rank}\left(\bigcup \left({A}×{B}\right)\right)\subseteq \mathrm{rank}\left({A}×{B}\right)$
9 7 8 sstri ${⊢}\mathrm{rank}\left(\bigcup \bigcup \left({A}×{B}\right)\right)\subseteq \mathrm{rank}\left({A}×{B}\right)$
10 4 9 eqsstrrdi ${⊢}{A}×{B}\ne \varnothing \to \mathrm{rank}\left({A}\cup {B}\right)\subseteq \mathrm{rank}\left({A}×{B}\right)$