Metamath Proof Explorer

Theorem rankunb

Description: The rank of the union of two sets. Theorem 15.17(iii) of Monk1 p. 112. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 unwf 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) )
2 rankval3b 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` ( A u. B ) ) = |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } )
3 1 2 sylbi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) = |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } )
4 3 eleq2d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) <-> x e. |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } ) )
5 vex 
 |-  x e. _V
6 5 elintrab 
 |-  ( x e. |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } <-> A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) )
7 4 6 bitrdi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) <-> A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) ) )
8 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
9 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
10 elun1 
 |-  ( ( rank ` x ) e. ( rank ` A ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) )
11 9 10 syl6 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
12 rankelb 
 |-  ( B e. U. ( R1 " On ) -> ( x e. B -> ( rank ` x ) e. ( rank ` B ) ) )
13 elun2 
 |-  ( ( rank ` x ) e. ( rank ` B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) )
14 12 13 syl6 
 |-  ( B e. U. ( R1 " On ) -> ( x e. B -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
15 11 14 jaao 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( x e. A \/ x e. B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
16 8 15 syl5bi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( A u. B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
17 16 ralrimiv 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) )
18 rankon 
 |-  ( rank ` A ) e. On
19 rankon 
 |-  ( rank ` B ) e. On
20 18 19 onun2i 
 |-  ( ( rank ` A ) u. ( rank ` B ) ) e. On
21 eleq2 
 |-  ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( ( rank ` x ) e. y <-> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
22 21 ralbidv 
 |-  ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. y <-> A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
23 eleq2 
 |-  ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( x e. y <-> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
24 22 23 imbi12d 
 |-  ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) <-> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) )
25 24 rspcv 
 |-  ( ( ( rank ` A ) u. ( rank ` B ) ) e. On -> ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) )
26 20 25 ax-mp 
 |-  ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
27 17 26 syl5com 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
28 7 27 sylbid 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) )
29 28 ssrdv 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) C_ ( ( rank ` A ) u. ( rank ` B ) ) )
30 ssun1 
 |-  A C_ ( A u. B )
31 rankssb 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( A C_ ( A u. B ) -> ( rank ` A ) C_ ( rank ` ( A u. B ) ) ) )
32 30 31 mpi 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` A ) C_ ( rank ` ( A u. B ) ) )
33 ssun2 
 |-  B C_ ( A u. B )
34 rankssb 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( B C_ ( A u. B ) -> ( rank ` B ) C_ ( rank ` ( A u. B ) ) ) )
35 33 34 mpi 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` B ) C_ ( rank ` ( A u. B ) ) )
36 32 35 unssd 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( ( rank ` A ) u. ( rank ` B ) ) C_ ( rank ` ( A u. B ) ) )
37 1 36 sylbi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) C_ ( rank ` ( A u. B ) ) )
38 29 37 eqssd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) )