Theorem rankprb

Description: The rank of an unordered pair. Part of Exercise 30 of Enderton p. 207. (Contributed by Mario Carneiro, 10-Jun-2013)

	Ref	Expression
Assertion	rankprb	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		snwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
2		snwf	⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
3		rankunb	⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) )
5		ranksnb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )
6		ranksnb	⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐵 } ) = suc ( rank ‘ 𝐵 ) )
7		uneq12	⊢ ( ( ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) ∧ ( rank ‘ { 𝐵 } ) = suc ( rank ‘ 𝐵 ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
8	5 6 7	syl2an	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
9	4 8	eqtrd	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
10		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
11	10	fveq2i	⊢ ( rank ‘ { 𝐴 , 𝐵 } ) = ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) )
12		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
13	12	onordi	⊢ Ord ( rank ‘ 𝐴 )
14		rankon	⊢ ( rank ‘ 𝐵 ) ∈ On
15	14	onordi	⊢ Ord ( rank ‘ 𝐵 )
16		ordsucun	⊢ ( ( Ord ( rank ‘ 𝐴 ) ∧ Ord ( rank ‘ 𝐵 ) ) → suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
17	13 15 16	mp2an	⊢ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) )
18	9 11 17	3eqtr4g	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )