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 e. _V
	rankxplim.2	|- B e. _V
Assertion	rankxpsuc	|- ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = suc suc ( rank ` ( A u. B ) ) )

Proof

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