Metamath Proof Explorer

Theorem rankelop

Description: Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypotheses rankelun.1 ⊢ A ∈ V
rankelun.2 ⊢ B ∈ V
rankelun.3 ⊢ C ∈ V
rankelun.4 ⊢ D ∈ V
Assertion rankelop ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A B ∈ rank ⁡ C D

Proof

Step Hyp Ref Expression
1 rankelun.1 ⊢ A ∈ V
2 rankelun.2 ⊢ B ∈ V
3 rankelun.3 ⊢ C ∈ V
4 rankelun.4 ⊢ D ∈ V
5 1 2 3 4 rankelpr ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A B ∈ rank ⁡ C D
6 rankon ⊢ rank ⁡ C D ∈ On
7 6 onordi ⊢ Ord ⁡ rank ⁡ C D
8 ordsucelsuc ⊢ Ord ⁡ rank ⁡ C D → rank ⁡ A B ∈ rank ⁡ C D ↔ suc ⁡ rank ⁡ A B ∈ suc ⁡ rank ⁡ C D
9 7 8 ax-mp ⊢ rank ⁡ A B ∈ rank ⁡ C D ↔ suc ⁡ rank ⁡ A B ∈ suc ⁡ rank ⁡ C D
10 5 9 sylib ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → suc ⁡ rank ⁡ A B ∈ suc ⁡ rank ⁡ C D
11 1 2 rankop ⊢ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
12 1 2 rankpr ⊢ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
13 suceq ⊢ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B → suc ⁡ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
14 12 13 ax-mp ⊢ suc ⁡ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
15 11 14 eqtr4i ⊢ rank ⁡ A B = suc ⁡ rank ⁡ A B
16 3 4 rankop ⊢ rank ⁡ C D = suc ⁡ suc ⁡ rank ⁡ C ∪ rank ⁡ D
17 3 4 rankpr ⊢ rank ⁡ C D = suc ⁡ rank ⁡ C ∪ rank ⁡ D
18 suceq ⊢ rank ⁡ C D = suc ⁡ rank ⁡ C ∪ rank ⁡ D → suc ⁡ rank ⁡ C D = suc ⁡ suc ⁡ rank ⁡ C ∪ rank ⁡ D
19 17 18 ax-mp ⊢ suc ⁡ rank ⁡ C D = suc ⁡ suc ⁡ rank ⁡ C ∪ rank ⁡ D
20 16 19 eqtr4i ⊢ rank ⁡ C D = suc ⁡ rank ⁡ C D
21 10 15 20 3eltr4g ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A B ∈ rank ⁡ C D