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 ‘ { 𝐶 , 𝐷 } ) )