Metamath Proof Explorer


Theorem rankuni

Description: The rank of a union. Part of Exercise 4 of Kunen p. 107. (Contributed by NM, 15-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankuni
|- ( rank ` U. A ) = U. ( rank ` A )

Proof

Step Hyp Ref Expression
1 unieq
 |-  ( x = A -> U. x = U. A )
2 1 fveq2d
 |-  ( x = A -> ( rank ` U. x ) = ( rank ` U. A ) )
3 fveq2
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
4 3 unieqd
 |-  ( x = A -> U. ( rank ` x ) = U. ( rank ` A ) )
5 2 4 eqeq12d
 |-  ( x = A -> ( ( rank ` U. x ) = U. ( rank ` x ) <-> ( rank ` U. A ) = U. ( rank ` A ) ) )
6 vex
 |-  x e. _V
7 6 rankuni2
 |-  ( rank ` U. x ) = U_ z e. x ( rank ` z )
8 fvex
 |-  ( rank ` z ) e. _V
9 8 dfiun2
 |-  U_ z e. x ( rank ` z ) = U. { y | E. z e. x y = ( rank ` z ) }
10 7 9 eqtri
 |-  ( rank ` U. x ) = U. { y | E. z e. x y = ( rank ` z ) }
11 df-rex
 |-  ( E. z e. x y = ( rank ` z ) <-> E. z ( z e. x /\ y = ( rank ` z ) ) )
12 6 rankel
 |-  ( z e. x -> ( rank ` z ) e. ( rank ` x ) )
13 12 anim1i
 |-  ( ( z e. x /\ y = ( rank ` z ) ) -> ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) )
14 13 eximi
 |-  ( E. z ( z e. x /\ y = ( rank ` z ) ) -> E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) )
15 19.42v
 |-  ( E. z ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) )
16 eleq1
 |-  ( y = ( rank ` z ) -> ( y e. ( rank ` x ) <-> ( rank ` z ) e. ( rank ` x ) ) )
17 16 pm5.32ri
 |-  ( ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) )
18 17 exbii
 |-  ( E. z ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) )
19 simpl
 |-  ( ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) -> y e. ( rank ` x ) )
20 rankon
 |-  ( rank ` x ) e. On
21 20 oneli
 |-  ( y e. ( rank ` x ) -> y e. On )
22 r1fnon
 |-  R1 Fn On
23 fndm
 |-  ( R1 Fn On -> dom R1 = On )
24 22 23 ax-mp
 |-  dom R1 = On
25 21 24 eleqtrrdi
 |-  ( y e. ( rank ` x ) -> y e. dom R1 )
26 rankr1id
 |-  ( y e. dom R1 <-> ( rank ` ( R1 ` y ) ) = y )
27 25 26 sylib
 |-  ( y e. ( rank ` x ) -> ( rank ` ( R1 ` y ) ) = y )
28 27 eqcomd
 |-  ( y e. ( rank ` x ) -> y = ( rank ` ( R1 ` y ) ) )
29 fvex
 |-  ( R1 ` y ) e. _V
30 fveq2
 |-  ( z = ( R1 ` y ) -> ( rank ` z ) = ( rank ` ( R1 ` y ) ) )
31 30 eqeq2d
 |-  ( z = ( R1 ` y ) -> ( y = ( rank ` z ) <-> y = ( rank ` ( R1 ` y ) ) ) )
32 29 31 spcev
 |-  ( y = ( rank ` ( R1 ` y ) ) -> E. z y = ( rank ` z ) )
33 28 32 syl
 |-  ( y e. ( rank ` x ) -> E. z y = ( rank ` z ) )
34 33 ancli
 |-  ( y e. ( rank ` x ) -> ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) )
35 19 34 impbii
 |-  ( ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) <-> y e. ( rank ` x ) )
36 15 18 35 3bitr3i
 |-  ( E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> y e. ( rank ` x ) )
37 14 36 sylib
 |-  ( E. z ( z e. x /\ y = ( rank ` z ) ) -> y e. ( rank ` x ) )
38 11 37 sylbi
 |-  ( E. z e. x y = ( rank ` z ) -> y e. ( rank ` x ) )
39 38 abssi
 |-  { y | E. z e. x y = ( rank ` z ) } C_ ( rank ` x )
40 39 unissi
 |-  U. { y | E. z e. x y = ( rank ` z ) } C_ U. ( rank ` x )
41 10 40 eqsstri
 |-  ( rank ` U. x ) C_ U. ( rank ` x )
42 pwuni
 |-  x C_ ~P U. x
43 vuniex
 |-  U. x e. _V
44 43 pwex
 |-  ~P U. x e. _V
45 44 rankss
 |-  ( x C_ ~P U. x -> ( rank ` x ) C_ ( rank ` ~P U. x ) )
46 42 45 ax-mp
 |-  ( rank ` x ) C_ ( rank ` ~P U. x )
47 43 rankpw
 |-  ( rank ` ~P U. x ) = suc ( rank ` U. x )
48 46 47 sseqtri
 |-  ( rank ` x ) C_ suc ( rank ` U. x )
49 48 unissi
 |-  U. ( rank ` x ) C_ U. suc ( rank ` U. x )
50 rankon
 |-  ( rank ` U. x ) e. On
51 50 onunisuci
 |-  U. suc ( rank ` U. x ) = ( rank ` U. x )
52 49 51 sseqtri
 |-  U. ( rank ` x ) C_ ( rank ` U. x )
53 41 52 eqssi
 |-  ( rank ` U. x ) = U. ( rank ` x )
54 5 53 vtoclg
 |-  ( A e. _V -> ( rank ` U. A ) = U. ( rank ` A ) )
55 uniexb
 |-  ( A e. _V <-> U. A e. _V )
56 fvprc
 |-  ( -. U. A e. _V -> ( rank ` U. A ) = (/) )
57 55 56 sylnbi
 |-  ( -. A e. _V -> ( rank ` U. A ) = (/) )
58 uni0
 |-  U. (/) = (/)
59 57 58 eqtr4di
 |-  ( -. A e. _V -> ( rank ` U. A ) = U. (/) )
60 fvprc
 |-  ( -. A e. _V -> ( rank ` A ) = (/) )
61 60 unieqd
 |-  ( -. A e. _V -> U. ( rank ` A ) = U. (/) )
62 59 61 eqtr4d
 |-  ( -. A e. _V -> ( rank ` U. A ) = U. ( rank ` A ) )
63 54 62 pm2.61i
 |-  ( rank ` U. A ) = U. ( rank ` A )