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

Metamath Proof Explorer

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