Metamath Proof Explorer

Theorem rankopb

Description: The rank of an ordered pair. Part of Exercise 4 of Kunen p. 107. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion rankopb 
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` <. A , B >. ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) )

Proof

Step Hyp Ref Expression
1 dfopg 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. = { { A } , { A , B } } )
2 1 fveq2d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` <. A , B >. ) = ( rank ` { { A } , { A , B } } ) )
3 snwf 
 |-  ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
4 prwf 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )
5 rankprb 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { A , B } e. U. ( R1 " On ) ) -> ( rank ` { { A } , { A , B } } ) = suc ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) )
6 3 4 5 syl2an2r 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` { { A } , { A , B } } ) = suc ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) )
7 snsspr1 
 |-  { A } C_ { A , B }
8 ssequn1 
 |-  ( { A } C_ { A , B } <-> ( { A } u. { A , B } ) = { A , B } )
9 7 8 mpbi 
 |-  ( { A } u. { A , B } ) = { A , B }
10 9 fveq2i 
 |-  ( rank ` ( { A } u. { A , B } ) ) = ( rank ` { A , B } )
11 rankunb 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { A , B } e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { A , B } ) ) = ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) )
12 3 4 11 syl2an2r 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { A , B } ) ) = ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) )
13 rankprb 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` { A , B } ) = suc ( ( rank ` A ) u. ( rank ` B ) ) )
14 10 12 13 3eqtr3a 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) = suc ( ( rank ` A ) u. ( rank ` B ) ) )
15 suceq 
 |-  ( ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) = suc ( ( rank ` A ) u. ( rank ` B ) ) -> suc ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) )
16 14 15 syl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> suc ( ( rank ` { A } ) u. ( rank ` { A , B } ) ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) )
17 2 6 16 3eqtrd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` <. A , B >. ) = suc suc ( ( rank ` A ) u. ( rank ` B ) ) )