Theorem rankxplim2

Description: If the rank of a Cartesian product is a limit ordinal, so is the rank of the union of its arguments. (Contributed by NM, 19-Sep-2006)

	Ref	Expression
Hypotheses	rankxplim.1	|- A e. _V
	rankxplim.2	|- B e. _V
Assertion	rankxplim2	|- ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankxplim.1	|- A e. _V
2		rankxplim.2	|- B e. _V
3		0ellim	|- ( Lim ( rank ` ( A X. B ) ) -> (/) e. ( rank ` ( A X. B ) ) )
4		n0i	|- ( (/) e. ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
5	3 4	syl	|- ( Lim ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
6		df-ne	|- ( ( A X. B ) =/= (/) <-> -. ( A X. B ) = (/) )
7	1 2	xpex	|- ( A X. B ) e. _V
8	7	rankeq0	|- ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) )
9	8	notbii	|- ( -. ( A X. B ) = (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
10	6 9	bitr2i	|- ( -. ( rank ` ( A X. B ) ) = (/) <-> ( A X. B ) =/= (/) )
11	5 10	sylib	|- ( Lim ( rank ` ( A X. B ) ) -> ( A X. B ) =/= (/) )
12		limuni2	|- ( Lim ( rank ` ( A X. B ) ) -> Lim U. ( rank ` ( A X. B ) ) )
13		limuni2	|- ( Lim U. ( rank ` ( A X. B ) ) -> Lim U. U. ( rank ` ( A X. B ) ) )
14	12 13	syl	|- ( Lim ( rank ` ( A X. B ) ) -> Lim U. U. ( rank ` ( A X. B ) ) )
15		rankuni	|- ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) )
16		rankuni	|- ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) )
17	16	unieqi	|- U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
18	15 17	eqtr2i	|- U. U. ( rank ` ( A X. B ) ) = ( rank ` U. U. ( A X. B ) )
19		unixp	|- ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
20	19	fveq2d	|- ( ( A X. B ) =/= (/) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
21	18 20	eqtrid	|- ( ( A X. B ) =/= (/) -> U. U. ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
22		limeq	|- ( U. U. ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) -> ( Lim U. U. ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
23	21 22	syl	|- ( ( A X. B ) =/= (/) -> ( Lim U. U. ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
24	14 23	imbitrid	|- ( ( A X. B ) =/= (/) -> ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) ) )
25	11 24	mpcom	|- ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) )