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\in \mathrm{V}$$
	rankxplim.2	$$⊢B\in \mathrm{V}$$
Assertion	rankxplim2	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankxplim.1	$$⊢A\in \mathrm{V}$$
2		rankxplim.2	$$⊢B\in \mathrm{V}$$
3		0ellim	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \varnothing \in \mathrm{rank}\left(A\times B\right)$$
4		n0i	$$⊢\varnothing \in \mathrm{rank}\left(A\times B\right)\to \neg \mathrm{rank}\left(A\times B\right)=\varnothing$$
5	3 4	syl	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \neg \mathrm{rank}\left(A\times B\right)=\varnothing$$
6		df-ne	$$⊢A\times B\ne \varnothing \leftrightarrow \neg A\times B=\varnothing$$
7	1 2	xpex	$$⊢A\times B\in \mathrm{V}$$
8	7	rankeq0	$$⊢A\times B=\varnothing \leftrightarrow \mathrm{rank}\left(A\times B\right)=\varnothing$$
9	8	notbii	$$⊢\neg A\times B=\varnothing \leftrightarrow \neg \mathrm{rank}\left(A\times B\right)=\varnothing$$
10	6 9	bitr2i	$$⊢\neg \mathrm{rank}\left(A\times B\right)=\varnothing \leftrightarrow A\times B\ne \varnothing$$
11	5 10	sylib	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to A\times B\ne \varnothing$$
12		limuni2	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)$$
13		limuni2	$$⊢\mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
14	12 13	syl	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
15		rankuni	$$⊢\mathrm{rank}\left(\bigcup \bigcup \left(A\times B\right)\right)=\bigcup \mathrm{rank}\left(\bigcup \left(A\times B\right)\right)$$
16		rankuni	$$⊢\mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
17	16	unieqi	$$⊢\bigcup \mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
18	15 17	eqtr2i	$$⊢\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(\bigcup \bigcup \left(A\times B\right)\right)$$
19		unixp	$$⊢A\times B\ne \varnothing \to \bigcup \bigcup \left(A\times B\right)=A\cup B$$
20	19	fveq2d	$$⊢A\times B\ne \varnothing \to \mathrm{rank}\left(\bigcup \bigcup \left(A\times B\right)\right)=\mathrm{rank}\left(A\cup B\right)$$
21	18 20	syl5eq	$$⊢A\times B\ne \varnothing \to \bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\cup B\right)$$
22		limeq	$$⊢\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\cup B\right)\to \left(\mathrm{Lim}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)\right)$$
23	21 22	syl	$$⊢A\times B\ne \varnothing \to \left(\mathrm{Lim}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)\right)$$
24	14 23	syl5ib	$$⊢A\times B\ne \varnothing \to \left(\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)\right)$$
25	11 24	mpcom	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)$$