This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )