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