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⁡AB∈rank⁡CD

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⁡AB=suc⁡rank⁡A∪rank⁡B
17 3 4 rankpr ⊢rank⁡CD=suc⁡rank⁡C∪rank⁡D
18 15 16 17 3eltr4g ⊢rank⁡A∈rank⁡C∧rank⁡B∈rank⁡D→rank⁡AB∈rank⁡CD