Metamath Proof Explorer

Theorem rankung

Description: The rank of the union of two sets. Closed form of rankun . (Contributed by Scott Fenton, 15-Jul-2015)

Ref Expression
Assertion rankung 
|- ( ( A e. V /\ B e. W ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) )

Proof

Step Hyp Ref Expression
1 uneq1 
 |-  ( x = A -> ( x u. y ) = ( A u. y ) )
2 1 fveq2d 
 |-  ( x = A -> ( rank ` ( x u. y ) ) = ( rank ` ( A u. y ) ) )
3 fveq2 
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
4 3 uneq1d 
 |-  ( x = A -> ( ( rank ` x ) u. ( rank ` y ) ) = ( ( rank ` A ) u. ( rank ` y ) ) )
5 2 4 eqeq12d 
 |-  ( x = A -> ( ( rank ` ( x u. y ) ) = ( ( rank ` x ) u. ( rank ` y ) ) <-> ( rank ` ( A u. y ) ) = ( ( rank ` A ) u. ( rank ` y ) ) ) )
6 uneq2 
 |-  ( y = B -> ( A u. y ) = ( A u. B ) )
7 6 fveq2d 
 |-  ( y = B -> ( rank ` ( A u. y ) ) = ( rank ` ( A u. B ) ) )
8 fveq2 
 |-  ( y = B -> ( rank ` y ) = ( rank ` B ) )
9 8 uneq2d 
 |-  ( y = B -> ( ( rank ` A ) u. ( rank ` y ) ) = ( ( rank ` A ) u. ( rank ` B ) ) )
10 7 9 eqeq12d 
 |-  ( y = B -> ( ( rank ` ( A u. y ) ) = ( ( rank ` A ) u. ( rank ` y ) ) <-> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) ) )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 11 12 rankun 
 |-  ( rank ` ( x u. y ) ) = ( ( rank ` x ) u. ( rank ` y ) )
14 5 10 13 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) )