Theorem rankxpu

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

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

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	⊢ 𝐴 ∈ V
2		rankxpl.2	⊢ 𝐵 ∈ V
3		xpsspw	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )
4	1 2	unex	⊢ ( 𝐴 ∪ 𝐵 ) ∈ V
5	4	pwex	⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ V
6	5	pwex	⊢ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ V
7	6	rankss	⊢ ( ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) → ( rank ‘ ( 𝐴 × 𝐵 ) ) ⊆ ( rank ‘ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) )
8	3 7	ax-mp	⊢ ( rank ‘ ( 𝐴 × 𝐵 ) ) ⊆ ( rank ‘ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) )
9	5	rankpw	⊢ ( rank ‘ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc ( rank ‘ 𝒫 ( 𝐴 ∪ 𝐵 ) )
10	4	rankpw	⊢ ( rank ‘ 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
11		suceq	⊢ ( ( rank ‘ 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) → suc ( rank ‘ 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
12	10 11	ax-mp	⊢ suc ( rank ‘ 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
13	9 12	eqtri	⊢ ( rank ‘ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
14	8 13	sseqtri	⊢ ( rank ‘ ( 𝐴 × 𝐵 ) ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )