Metamath Proof Explorer

Theorem rankelpr

Description: Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses rankelun.1 ⊢ A ∈ V
rankelun.2 ⊢ B ∈ V
rankelun.3 ⊢ C ∈ V
rankelun.4 ⊢ D ∈ V
Assertion rankelpr ⊢ 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 rankelun ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A ∪ B ∈ rank ⁡ C ∪ D
6 1 2 rankun ⊢ rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B
7 3 4 rankun ⊢ rank ⁡ C ∪ D = rank ⁡ C ∪ rank ⁡ D
8 5 6 7 3eltr3g ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A ∪ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D
9 rankon ⊢ rank ⁡ C ∈ On
10 rankon ⊢ rank ⁡ D ∈ On
11 9 10 onun2i ⊢ rank ⁡ C ∪ rank ⁡ D ∈ On
12 11 onordi ⊢ Ord ⁡ rank ⁡ C ∪ rank ⁡ D
13 ordsucelsuc ⊢ Ord ⁡ rank ⁡ C ∪ rank ⁡ D → rank ⁡ A ∪ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D ↔ suc ⁡ rank ⁡ A ∪ rank ⁡ B ∈ suc ⁡ rank ⁡ C ∪ rank ⁡ D
14 12 13 ax-mp ⊢ rank ⁡ A ∪ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D ↔ suc ⁡ rank ⁡ A ∪ rank ⁡ B ∈ suc ⁡ rank ⁡ C ∪ rank ⁡ D
15 8 14 sylib ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → suc ⁡ rank ⁡ A ∪ rank ⁡ B ∈ suc ⁡ rank ⁡ C ∪ rank ⁡ D
16 1 2 rankpr ⊢ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
17 3 4 rankpr ⊢ rank ⁡ C D = suc ⁡ rank ⁡ C ∪ rank ⁡ D
18 15 16 17 3eltr4g ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A B ∈ rank ⁡ C D