This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝐴 ∪ 𝐵 ) )