Theorem rankxpsuc 4695

Description: The rank of a cross product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 4692 for the limit ordinal case.

Hypotheses

Ref	Expression
rankxplim.1	|- A e. V
rankxplim.2	|- B e. V

Assertion

Ref	Expression
rankxpsuc	|- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> (rank` (A X. B)) = suc suc (rank` (A u. B)))

Proof of Theorem rankxpsuc

Step	Hyp	Ref	Expression
1		unixp 3509	. . . . . . . 8 |- ((A X. B) =/= (/) -> U.U.(A X. B) = (A u. B))
2	1	fveq2d 3719	. . . . . . 7 |- ((A X. B) =/= (/) -> (rank` U.U.(A X. B)) = (rank` (A u. B)))
3		rankuni 4678	. . . . . . . 8 |- (rank` U.U.(A X. B)) = U.(rank` U.(A X. B))
4		rankuni 4678	. . . . . . . . 9 |- (rank` U.(A X. B)) = U.(rank` (A X. B))
5	4	unieqi 2506	. . . . . . . 8 |- U.(rank` U.(A X. B)) = U.U.(rank` (A X. B))
6	3, 5	eqtr 1492	. . . . . . 7 |- (rank` U.U.(A X. B)) = U.U.(rank` (A X. B))
7	2, 6	syl5reqr 1519	. . . . . 6 |- ((A X. B) =/= (/) -> (rank` (A u. B)) = U.U.(rank` (A X. B)))
8		suc11reg 4585	. . . . . 6 |- (suc (rank` (A u. B)) = suc U.U.(rank` (A X. B)) <-> (rank` (A u. B)) = U.U.(rank` (A X. B)))
9	7, 8	sylibr 200	. . . . 5 |- ((A X. B) =/= (/) -> suc (rank` (A u. B)) = suc U.U.(rank` (A X. B)))
10	9	adantl 388	. . . 4 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc (rank` (A u. B)) = suc U.U.(rank` (A X. B)))
11		fvex 3723	. . . . . . . . . . . . 13 |- (rank` (A u. B)) e. V
12		eleq1 1531	. . . . . . . . . . . . 13 |- ((rank` (A u. B)) = suc C -> ((rank` (A u. B)) e. V <-> suc C e. V))
13	11, 12	mpbii 193	. . . . . . . . . . . 12 |- ((rank` (A u. B)) = suc C -> suc C e. V)
14		sucexb 3043	. . . . . . . . . . . 12 |- (C e. V <-> suc C e. V)
15	13, 14	sylibr 200	. . . . . . . . . . 11 |- ((rank` (A u. B)) = suc C -> C e. V)
16		nlimsucg 3107	. . . . . . . . . . 11 |- (C e. V -> -. Lim suc C)
17	15, 16	syl 10	. . . . . . . . . 10 |- ((rank` (A u. B)) = suc C -> -. Lim suc C)
18		limeq 2955	. . . . . . . . . 10 |- ((rank` (A u. B)) = suc C -> (Lim (rank` (A u. B)) <-> Lim suc C))
19	17, 18	mtbird 714	. . . . . . . . 9 |- ((rank` (A u. B)) = suc C -> -. Lim (rank` (A u. B)))
20		rankxplim.1	. . . . . . . . . . 11 |- A e. V
21		rankxplim.2	. . . . . . . . . . 11 |- B e. V
22	20, 21	rankxplim2 4693	. . . . . . . . . 10 |- (Lim (rank` (A X. B)) -> Lim (rank` (A u. B)))
23	22	con3i 98	. . . . . . . . 9 |- (-. Lim (rank` (A u. B)) -> -. Lim (rank` (A X. B)))
24	20, 21	xpex 3255	. . . . . . . . . . . . . . 15 |- (A X. B) e. V
25	24	rankeq0 4676	. . . . . . . . . . . . . 14 |- ((A X. B) = (/) <-> (rank` (A X. B)) = (/))
26	25	necon3abii 1593	. . . . . . . . . . . . 13 |- ((A X. B) =/= (/) <-> -. (rank` (A X. B)) = (/))
27		rankon 4651	. . . . . . . . . . . . . . . . 17 |- (rank` (A X. B)) e. On
28	27	onord 3090	. . . . . . . . . . . . . . . 16 |- Ord (rank` (A X. B))
29		ordzsl 3111	. . . . . . . . . . . . . . . 16 |- (Ord (rank` (A X. B)) <-> ((rank` (A X. B)) = (/) \/ E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
30	28, 29	mpbi 189	. . . . . . . . . . . . . . 15 |- ((rank` (A X. B)) = (/) \/ E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B)))
31		3orass 777	. . . . . . . . . . . . . . 15 |- (((rank` (A X. B)) = (/) \/ E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))) <-> ((rank` (A X. B)) = (/) \/ (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B)))))
32	30, 31	mpbi 189	. . . . . . . . . . . . . 14 |- ((rank` (A X. B)) = (/) \/ (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
33	32	ori 230	. . . . . . . . . . . . 13 |- (-. (rank` (A X. B)) = (/) -> (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
34	26, 33	sylbi 199	. . . . . . . . . . . 12 |- ((A X. B) =/= (/) -> (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
35	34	ord 232	. . . . . . . . . . 11 |- ((A X. B) =/= (/) -> (-. E.x e. On (rank` (A X. B)) = suc x -> Lim (rank` (A X. B))))
36	35	con1d 93	. . . . . . . . . 10 |- ((A X. B) =/= (/) -> (-. Lim (rank` (A X. B)) -> E.x e. On (rank` (A X. B)) = suc x))
37	36	com12 11	. . . . . . . . 9 |- (-. Lim (rank` (A X. B)) -> ((A X. B) =/= (/) -> E.x e. On (rank` (A X. B)) = suc x))
38	19, 23, 37	3syl 20	. . . . . . . 8 |- ((rank` (A u. B)) = suc C -> ((A X. B) =/= (/) -> E.x e. On (rank` (A X. B)) = suc x))
39		visset 1809	. . . . . . . . . . . . 13 |- x e. V
40		nlimsucg 3107	. . . . . . . . . . . . 13 |- (x e. V -> -. Lim suc x)
41	39, 40	ax-mp 7	. . . . . . . . . . . 12 |- -. Lim suc x
42		limeq 2955	. . . . . . . . . . . 12 |- ((rank` (A X. B)) = suc x -> (Lim (rank` (A X. B)) <-> Lim suc x))
43	41, 42	mtbiri 716	. . . . . . . . . . 11 |- ((rank` (A X. B)) = suc x -> -. Lim (rank` (A X. B)))
44	43	a1i 8	. . . . . . . . . 10 |- (x e. On -> ((rank` (A X. B)) = suc x -> -. Lim (rank` (A X. B))))
45	44	r19.23aiv 1740	. . . . . . . . 9 |- (E.x e. On (rank` (A X. B)) = suc x -> -. Lim (rank` (A X. B)))
46	20, 21	rankxplim3 4694	. . . . . . . . . 10 |- (Lim (rank` (A X. B)) <-> Lim U.(rank` (A X. B)))
47	46	negbii 187	. . . . . . . . 9 |- (-. Lim (rank` (A X. B)) <-> -. Lim U.(rank` (A X. B)))
48	45, 47	sylib 198	. . . . . . . 8 |- (E.x e. On (rank` (A X. B)) = suc x -> -. Lim U.(rank` (A X. B)))
49	38, 48	syl6com 53	. . . . . . 7 |- ((A X. B) =/= (/) -> ((rank` (A u. B)) = suc C -> -. Lim U.(rank` (A X. B))))
50		unixp0 3510	. . . . . . . . . . . 12 |- ((A X. B) = (/) <-> U.(A X. B) = (/))
51	24	uniex 2865	. . . . . . . . . . . . 13 |- U.(A X. B) e. V
52	51	rankeq0 4676	. . . . . . . . . . . 12 |- (U.(A X. B) = (/) <-> (rank` U.(A X. B)) = (/))
53	4	eqeq1i 1479	. . . . . . . . . . . 12 |- ((rank` U.(A X. B)) = (/) <-> U.(rank` (A X. B)) = (/))
54	50, 52, 53	3bitr 177	. . . . . . . . . . 11 |- ((A X. B) = (/) <-> U.(rank` (A X. B)) = (/))
55	54	necon3abii 1593	. . . . . . . . . 10 |- ((A X. B) =/= (/) <-> -. U.(rank` (A X. B)) = (/))
56		onuni 2991	. . . . . . . . . . . . . . 15 |- ((rank` (A X. B)) e. On -> U.(rank` (A X. B)) e. On)
57	27, 56	ax-mp 7	. . . . . . . . . . . . . 14 |- U.(rank` (A X. B)) e. On
58	57	onord 3090	. . . . . . . . . . . . 13 |- Ord U.(rank` (A X. B))
59		ordzsl 3111	. . . . . . . . . . . . 13 |- (Ord U.(rank` (A X. B)) <-> (U.(rank` (A X. B)) = (/) \/ E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))))
60	58, 59	mpbi 189	. . . . . . . . . . . 12 |- (U.(rank` (A X. B)) = (/) \/ E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B)))
61		3orass 777	. . . . . . . . . . . 12 |- ((U.(rank` (A X. B)) = (/) \/ E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))) <-> (U.(rank` (A X. B)) = (/) \/ (E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B)))))
62	60, 61	mpbi 189	. . . . . . . . . . 11 |- (U.(rank` (A X. B)) = (/) \/ (E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))))
63	62	ori 230	. . . . . . . . . 10 |- (-. U.(rank` (A X. B)) = (/) -> (E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))))
64	55, 63	sylbi 199	. . . . . . . . 9 |- ((A X. B) =/= (/) -> (E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))))
65	64	ord 232	. . . . . . . 8 |- ((