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 ⊢ A ∈ V
rankxpl.2 ⊢ B ∈ V
Assertion rankxpu ⊢ rank ⁡ A × B ⊆ suc ⁡ suc ⁡ rank ⁡ A ∪ B

Proof

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