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

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 ⊢ 𝐴 ∈ V
rankelun.2 ⊢ 𝐵 ∈ V
rankelun.3 ⊢ 𝐶 ∈ V
rankelun.4 ⊢ 𝐷 ∈ V
Assertion rankelpr ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) ∈ ( rank ‘ { 𝐶 , 𝐷 } ) )

Proof

Step Hyp Ref Expression
1 rankelun.1 ⊢ 𝐴 ∈ V
2 rankelun.2 ⊢ 𝐵 ∈ V
3 rankelun.3 ⊢ 𝐶 ∈ V
4 rankelun.4 ⊢ 𝐷 ∈ V
5 1 2 3 4 rankelun ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ( rank ‘ ( 𝐶 ∪ 𝐷 ) ) )
6 1 2 rankun ⊢ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
7 3 4 rankun ⊢ ( rank ‘ ( 𝐶 ∪ 𝐷 ) ) = ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
8 5 6 7 3eltr3g ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) )
9 rankon ⊢ ( rank ‘ 𝐶 ) ∈ On
10 rankon ⊢ ( rank ‘ 𝐷 ) ∈ On
11 9 10 onun2i ⊢ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ∈ On
12 11 onordi ⊢ Ord ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
13 ordsucelsuc ⊢ ( Ord ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) → ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ↔ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) )
14 12 13 ax-mp ⊢ ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ↔ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) )
15 8 14 sylib ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) )
16 1 2 rankpr ⊢ ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
17 3 4 rankpr ⊢ ( rank ‘ { 𝐶 , 𝐷 } ) = suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
18 15 16 17 3eltr4g ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) ∈ ( rank ‘ { 𝐶 , 𝐷 } ) )