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 )