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 V$
	rankxpl.2	$⊢ B \in V$
Assertion	rankxpl	$⊢ A \times B \neq \emptyset \to rank (A \cup B) \subseteq rank (A \times B)$

Step	Hyp	Ref	Expression
1		rankxpl.1	$⊢ A \in V$
2		rankxpl.2	$⊢ B \in V$
3		unixp	$⊢ A \times B \neq \emptyset \to ⋃ ⋃ (A \times B) = A \cup B$
4	3	fveq2d	$⊢ A \times B \neq \emptyset \to rank (⋃ ⋃ (A \times B)) = rank (A \cup B)$
5	1 2	xpex	$⊢ A \times B \in V$
6	5	uniex	$⊢ ⋃ (A \times B) \in V$
7	6	rankuniss	$⊢ rank (⋃ ⋃ (A \times B)) \subseteq rank (⋃ (A \times B))$
8	5	rankuniss	$⊢ rank (⋃ (A \times B)) \subseteq rank (A \times B)$
9	7 8	sstri	$⊢ rank (⋃ ⋃ (A \times B)) \subseteq rank (A \times B)$
10	4 9	eqsstrrdi	$⊢ A \times B \neq \emptyset \to rank (A \cup B) \subseteq rank (A \times B)$

Metamath Proof Explorer