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	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		snwf	|- ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
2		snwf	|- ( B e. U. ( R1 " On ) -> { B } e. U. ( R1 " On ) )
3		rankunb	|- ( ( { A } e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { B } ) ) = ( ( rank ` { A } ) u. ( rank ` { B } ) ) )
4	1 2 3	syl2an	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { B } ) ) = ( ( rank ` { A } ) u. ( rank ` { B } ) ) )
5		ranksnb	|- ( A e. U. ( R1 " On ) -> ( rank ` { A } ) = suc ( rank ` A ) )
6		ranksnb	|- ( B e. U. ( R1 " On ) -> ( rank ` { B } ) = suc ( rank ` B ) )
7		uneq12	|- ( ( ( rank ` { A } ) = suc ( rank ` A ) /\ ( rank ` { B } ) = suc ( rank ` B ) ) -> ( ( rank ` { A } ) u. ( rank ` { B } ) ) = ( suc ( rank ` A ) u. suc ( rank ` B ) ) )
8	5 6 7	syl2an	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( rank ` { A } ) u. ( rank ` { B } ) ) = ( suc ( rank ` A ) u. suc ( rank ` B ) ) )
9	4 8	eqtrd	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { B } ) ) = ( suc ( rank ` A ) u. suc ( rank ` B ) ) )
10		df-pr	|- { A , B } = ( { A } u. { B } )
11	10	fveq2i	|- ( rank ` { A , B } ) = ( rank ` ( { A } u. { B } ) )
12		rankon	|- ( rank ` A ) e. On
13	12	onordi	|- Ord ( rank ` A )
14		rankon	|- ( rank ` B ) e. On
15	14	onordi	|- Ord ( rank ` B )
16		ordsucun	|- ( ( Ord ( rank ` A ) /\ Ord ( rank ` B ) ) -> suc ( ( rank ` A ) u. ( rank ` B ) ) = ( suc ( rank ` A ) u. suc ( rank ` B ) ) )
17	13 15 16	mp2an	|- suc ( ( rank ` A ) u. ( rank ` B ) ) = ( suc ( rank ` A ) u. suc ( rank ` B ) )
18	9 11 17	3eqtr4g	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) ) )