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

Metamath Proof Explorer

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 ) ) )