Metamath Proof Explorer

Theorem rankaltopb

Description: Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 snwf 
 |-  ( B e. U. ( R1 " On ) -> { B } e. U. ( R1 " On ) )
2 df-altop 
 |-  << A , B >> = { { A } , { A , { B } } }
3 2 fveq2i 
 |-  ( rank ` << A , B >> ) = ( rank ` { { A } , { A , { B } } } )
4 snwf 
 |-  ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
5 4 adantr 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> { A } e. U. ( R1 " On ) )
6 prwf 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> { A , { B } } e. U. ( R1 " On ) )
7 rankprb 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { A , { B } } e. U. ( R1 " On ) ) -> ( rank ` { { A } , { A , { B } } } ) = suc ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) )
8 5 6 7 syl2anc 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` { { A } , { A , { B } } } ) = suc ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) )
9 3 8 eqtrid 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` << A , B >> ) = suc ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) )
10 snsspr1 
 |-  { A } C_ { A , { B } }
11 ssequn1 
 |-  ( { A } C_ { A , { B } } <-> ( { A } u. { A , { B } } ) = { A , { B } } )
12 10 11 mpbi 
 |-  ( { A } u. { A , { B } } ) = { A , { B } }
13 12 fveq2i 
 |-  ( rank ` ( { A } u. { A , { B } } ) ) = ( rank ` { A , { B } } )
14 rankunb 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { A , { B } } e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { A , { B } } ) ) = ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) )
15 5 6 14 syl2anc 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` ( { A } u. { A , { B } } ) ) = ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) )
16 rankprb 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` { A , { B } } ) = suc ( ( rank ` A ) u. ( rank ` { B } ) ) )
17 13 15 16 3eqtr3a 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( ( rank ` { A } ) u. ( rank ` { A , { B } } ) ) = suc ( ( rank ` A ) u. ( rank ` { B } ) ) )
18 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 } ) ) )
19 17 18 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 } ) ) )
20 9 19 eqtrd 
 |-  ( ( A e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( rank ` << A , B >> ) = suc suc ( ( rank ` A ) u. ( rank ` { B } ) ) )
21 1 20 sylan2 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` << A , B >> ) = suc suc ( ( rank ` A ) u. ( rank ` { B } ) ) )
22 ranksnb 
 |-  ( B e. U. ( R1 " On ) -> ( rank ` { B } ) = suc ( rank ` B ) )
23 22 uneq2d 
 |-  ( B e. U. ( R1 " On ) -> ( ( rank ` A ) u. ( rank ` { B } ) ) = ( ( rank ` A ) u. suc ( rank ` B ) ) )
24 suceq 
 |-  ( ( ( rank ` A ) u. ( rank ` { B } ) ) = ( ( rank ` A ) u. suc ( rank ` B ) ) -> suc ( ( rank ` A ) u. ( rank ` { B } ) ) = suc ( ( rank ` A ) u. suc ( rank ` B ) ) )
25 suceq 
 |-  ( suc ( ( rank ` A ) u. ( rank ` { B } ) ) = suc ( ( rank ` A ) u. suc ( rank ` B ) ) -> suc suc ( ( rank ` A ) u. ( rank ` { B } ) ) = suc suc ( ( rank ` A ) u. suc ( rank ` B ) ) )
26 23 24 25 3syl 
 |-  ( B e. U. ( R1 " On ) -> suc suc ( ( rank ` A ) u. ( rank ` { B } ) ) = suc suc ( ( rank ` A ) u. suc ( rank ` B ) ) )
27 26 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> suc suc ( ( rank ` A ) u. ( rank ` { B } ) ) = suc suc ( ( rank ` A ) u. suc ( rank ` B ) ) )
28 21 27 eqtrd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` << A , B >> ) = suc suc ( ( rank ` A ) u. suc ( rank ` B ) ) )