Theorem rankxpl

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

	Ref	Expression
Hypotheses	rankxpl.1	⊢ 𝐴 ∈ V
	rankxpl.2	⊢ 𝐵 ∈ V
Assertion	rankxpl	⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 × 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	⊢ 𝐴 ∈ V
2		rankxpl.2	⊢ 𝐵 ∈ V
3		unixp	⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ∪ ∪ ( 𝐴 × 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )
4	3	fveq2d	⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
5	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
6	5	uniex	⊢ ∪ ( 𝐴 × 𝐵 ) ∈ V
7	6	rankuniss	⊢ ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) ) ⊆ ( rank ‘ ∪ ( 𝐴 × 𝐵 ) )
8	5	rankuniss	⊢ ( rank ‘ ∪ ( 𝐴 × 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 × 𝐵 ) )
9	7 8	sstri	⊢ ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 × 𝐵 ) )
10	4 9	eqsstrrdi	⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 × 𝐵 ) ) )