Theorem rankxpsuc

Description: The rank of a Cartesian product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of Kunen p. 107. See rankxplim for the limit ordinal case. (Contributed by NM, 19-Sep-2006)

	Ref	Expression
Hypotheses	rankxplim.1	$$⊢A\in \mathrm{V}$$
	rankxplim.2	$$⊢B\in \mathrm{V}$$
Assertion	rankxpsuc	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{rank}\left(A\times B\right)=\mathrm{suc}\mathrm{suc}\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		rankuni	$$⊢\mathrm{rank}\left(\bigcup \bigcup \left(A\times B\right)\right)=\bigcup \mathrm{rank}\left(\bigcup \left(A\times B\right)\right)$$
4		rankuni	$$⊢\mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
5	4	unieqi	$$⊢\bigcup \mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
6	3 5	eqtri	$$⊢\mathrm{rank}\left(\bigcup \bigcup \left(A\times B\right)\right)=\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
7		unixp	$$⊢A\times B\ne \varnothing \to \bigcup \bigcup \left(A\times B\right)=A\cup B$$
8	7	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)$$
9	6 8	syl5reqr	$$⊢A\times B\ne \varnothing \to \mathrm{rank}\left(A\cup B\right)=\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
10		suc11reg	$$⊢\mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{rank}\left(A\cup B\right)=\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
11	9 10	sylibr	$$⊢A\times B\ne \varnothing \to \mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
12	11	adantl	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)$$
13		fvex	$$⊢\mathrm{rank}\left(A\cup B\right)\in \mathrm{V}$$
14		eleq1	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \left(\mathrm{rank}\left(A\cup B\right)\in \mathrm{V}\leftrightarrow \mathrm{suc}C\in \mathrm{V}\right)$$
15	13 14	mpbii	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \mathrm{suc}C\in \mathrm{V}$$
16		sucexb	$$⊢C\in \mathrm{V}\leftrightarrow \mathrm{suc}C\in \mathrm{V}$$
17	15 16	sylibr	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to C\in \mathrm{V}$$
18		nlimsucg	$$⊢C\in \mathrm{V}\to \neg \mathrm{Lim}\mathrm{suc}C$$
19	17 18	syl	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \neg \mathrm{Lim}\mathrm{suc}C$$
20		limeq	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \left(\mathrm{Lim}\mathrm{rank}\left(A\cup B\right)\leftrightarrow \mathrm{Lim}\mathrm{suc}C\right)$$
21	19 20	mtbird	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \neg \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)$$
22	1 2	rankxplim2	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \mathrm{Lim}\mathrm{rank}\left(A\cup B\right)$$
23	21 22	nsyl	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \neg \mathrm{Lim}\mathrm{rank}\left(A\times B\right)$$
24	1 2	xpex	$$⊢A\times B\in \mathrm{V}$$
25	24	rankeq0	$$⊢A\times B=\varnothing \leftrightarrow \mathrm{rank}\left(A\times B\right)=\varnothing$$
26	25	necon3abii	$$⊢A\times B\ne \varnothing \leftrightarrow \neg \mathrm{rank}\left(A\times B\right)=\varnothing$$
27		rankon	$$⊢\mathrm{rank}\left(A\times B\right)\in \mathrm{On}$$
28	27	onordi	$$⊢\mathrm{Ord}\mathrm{rank}\left(A\times B\right)$$
29		ordzsl	$$⊢\mathrm{Ord}\mathrm{rank}\left(A\times B\right)\leftrightarrow \left(\mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)$$
30	28 29	mpbi	$$⊢\left(\mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)$$
31		3orass	$$⊢\left(\mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)\leftrightarrow \left(\mathrm{rank}\left(A\times B\right)=\varnothing \vee \left(\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)\right)$$
32	30 31	mpbi	$$⊢\left(\mathrm{rank}\left(A\times B\right)=\varnothing \vee \left(\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)\right)$$
33	32	ori	$$⊢\neg \mathrm{rank}\left(A\times B\right)=\varnothing \to \left(\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)$$
34	26 33	sylbi	$$⊢A\times B\ne \varnothing \to \left(\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)$$
35	34	ord	$$⊢A\times B\ne \varnothing \to \left(\neg \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\right)$$
36	35	con1d	$$⊢A\times B\ne \varnothing \to \left(\neg \mathrm{Lim}\mathrm{rank}\left(A\times B\right)\to \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)$$
37	23 36	syl5com	$$⊢\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \left(A\times B\ne \varnothing \to \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)$$
38		nlimsucg	$$⊢x\in \mathrm{V}\to \neg \mathrm{Lim}\mathrm{suc}x$$
39	38	elv	$$⊢\neg \mathrm{Lim}\mathrm{suc}x$$
40		limeq	$$⊢\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \left(\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{Lim}\mathrm{suc}x\right)$$
41	39 40	mtbiri	$$⊢\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \neg \mathrm{Lim}\mathrm{rank}\left(A\times B\right)$$
42	41	rexlimivw	$$⊢\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \neg \mathrm{Lim}\mathrm{rank}\left(A\times B\right)$$
43	1 2	rankxplim3	$$⊢\mathrm{Lim}\mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)$$
44	42 43	sylnib	$$⊢\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \neg \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)$$
45	37 44	syl6com	$$⊢A\times B\ne \varnothing \to \left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \neg \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
46		unixp0	$$⊢A\times B=\varnothing \leftrightarrow \bigcup \left(A\times B\right)=\varnothing$$
47	24	uniex	$$⊢\bigcup \left(A\times B\right)\in \mathrm{V}$$
48	47	rankeq0	$$⊢\bigcup \left(A\times B\right)=\varnothing \leftrightarrow \mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\varnothing$$
49	4	eqeq1i	$$⊢\mathrm{rank}\left(\bigcup \left(A\times B\right)\right)=\varnothing \leftrightarrow \bigcup \mathrm{rank}\left(A\times B\right)=\varnothing$$
50	46 48 49	3bitri	$$⊢A\times B=\varnothing \leftrightarrow \bigcup \mathrm{rank}\left(A\times B\right)=\varnothing$$
51	50	necon3abii	$$⊢A\times B\ne \varnothing \leftrightarrow \neg \bigcup \mathrm{rank}\left(A\times B\right)=\varnothing$$
52		onuni	$$⊢\mathrm{rank}\left(A\times B\right)\in \mathrm{On}\to \bigcup \mathrm{rank}\left(A\times B\right)\in \mathrm{On}$$
53	27 52	ax-mp	$$⊢\bigcup \mathrm{rank}\left(A\times B\right)\in \mathrm{On}$$
54	53	onordi	$$⊢\mathrm{Ord}\bigcup \mathrm{rank}\left(A\times B\right)$$
55		ordzsl	$$⊢\mathrm{Ord}\bigcup \mathrm{rank}\left(A\times B\right)\leftrightarrow \left(\bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
56	54 55	mpbi	$$⊢\left(\bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
57		3orass	$$⊢\left(\bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \vee \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)\leftrightarrow \left(\bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \vee \left(\exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)\right)$$
58	56 57	mpbi	$$⊢\left(\bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \vee \left(\exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)\right)$$
59	58	ori	$$⊢\neg \bigcup \mathrm{rank}\left(A\times B\right)=\varnothing \to \left(\exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
60	51 59	sylbi	$$⊢A\times B\ne \varnothing \to \left(\exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\vee \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
61	60	ord	$$⊢A\times B\ne \varnothing \to \left(\neg \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\right)$$
62	61	con1d	$$⊢A\times B\ne \varnothing \to \left(\neg \mathrm{Lim}\bigcup \mathrm{rank}\left(A\times B\right)\to \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)$$
63	45 62	syld	$$⊢A\times B\ne \varnothing \to \left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\to \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)$$
64	63	impcom	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x$$
65		onsucuni2	$$⊢\left(\bigcup \mathrm{rank}\left(A\times B\right)\in \mathrm{On}\wedge \bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)\to \mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
66	53 65	mpan	$$⊢\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
67	66	rexlimivw	$$⊢\exists x\in \mathrm{On}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
68	64 67	syl	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{suc}\bigcup \bigcup \mathrm{rank}\left(A\times B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
69	12 68	eqtrd	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
70		suc11reg	$$⊢\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)\leftrightarrow \mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\bigcup \mathrm{rank}\left(A\times B\right)$$
71	69 70	sylibr	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)$$
72	37	imp	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x$$
73		onsucuni2	$$⊢\left(\mathrm{rank}\left(A\times B\right)\in \mathrm{On}\wedge \mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\right)\to \mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\times B\right)$$
74	27 73	mpan	$$⊢\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\times B\right)$$
75	74	rexlimivw	$$⊢\exists x\in \mathrm{On}\mathrm{rank}\left(A\times B\right)=\mathrm{suc}x\to \mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\times B\right)$$
76	72 75	syl	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{suc}\bigcup \mathrm{rank}\left(A\times B\right)=\mathrm{rank}\left(A\times B\right)$$
77	71 76	eqtr2d	$$⊢\left(\mathrm{rank}\left(A\cup B\right)=\mathrm{suc}C\wedge A\times B\ne \varnothing \right)\to \mathrm{rank}\left(A\times B\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$