Theorem rankxpsuc 5826

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 5823 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 4422	. . . . . . . 8 |- ((A X. B) =/= (/) -> U.U.(A X. B) = (A u. B))
2	1	fveq2d 4685	. . . . . . 7 |- ((A X. B) =/= (/) -> (rank` U.U.(A X. B)) = (rank` (A u. B)))
3		rankuni 5809	. . . . . . . 8 |- (rank` U.U.(A X. B)) = U.(rank` U.(A X. B))
4		rankuni 5809	. . . . . . . . 9 |- (rank` U.(A X. B)) = U.(rank` (A X. B))
5	4	unieqi 3187	. . . . . . . 8 |- U.(rank` U.(A X. B)) = U.U.(rank` (A X. B))
6	3, 5	eqtri 1908	. . . . . . 7 |- (rank` U.U.(A X. B)) = U.U.(rank` (A X. B))
7	2, 6	syl5reqr 1943	. . . . . 6 |- ((A X. B) =/= (/) -> (rank` (A u. B)) = U.U.(rank` (A X. B)))
8		suc11reg 5710	. . . . . 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 217	. . . . 5 |- ((A X. B) =/= (/) -> suc (rank` (A u. B)) = suc U.U.(rank` (A X. B)))
10	9	adantl 424	. . . 4 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc (rank` (A u. B)) = suc U.U.(rank` (A X. B)))
11		fvex 4689	. . . . . . . . . . . . 13 |- (rank` (A u. B)) e. _V
12		eleq1 1957	. . . . . . . . . . . . 13 |- ((rank` (A u. B)) = suc C -> ((rank` (A u. B)) e. _V <-> suc C e. _V))
13	11, 12	mpbii 210	. . . . . . . . . . . 12 |- ((rank` (A u. B)) = suc C -> suc C e. _V)
14		sucexb 3890	. . . . . . . . . . . 12 |- (C e. _V <-> suc C e. _V)
15	13, 14	sylibr 217	. . . . . . . . . . 11 |- ((rank` (A u. B)) = suc C -> C e. _V)
16		nlimsucg 3923	. . . . . . . . . . 11 |- (C e. _V -> -. Lim suc C)
17	15, 16	syl 12	. . . . . . . . . 10 |- ((rank` (A u. B)) = suc C -> -. Lim suc C)
18		limeq 3669	. . . . . . . . . 10 |- ((rank` (A u. B)) = suc C -> (Lim (rank` (A u. B)) <-> Lim suc C))
19	17, 18	mtbird 783	. . . . . . . . 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 5824	. . . . . . . . . 10 |- (Lim (rank` (A X. B)) -> Lim (rank` (A u. B)))
23	22	con3i 114	. . . . . . . . 9 |- (-. Lim (rank` (A u. B)) -> -. Lim (rank` (A X. B)))
24	20, 21	xpex 4096	. . . . . . . . . . . . . . 15 |- (A X. B) e. _V
25	24	rankeq0 5807	. . . . . . . . . . . . . 14 |- ((A X. B) = (/) <-> (rank` (A X. B)) = (/))
26	25	necon3abii 2030	. . . . . . . . . . . . 13 |- ((A X. B) =/= (/) <-> -. (rank` (A X. B)) = (/))
27		rankon 5782	. . . . . . . . . . . . . . . . 17 |- (rank` (A X. B)) e. On
28	27	onordi 3774	. . . . . . . . . . . . . . . 16 |- Ord (rank` (A X. B))
29		ordzsl 3927	. . . . . . . . . . . . . . . 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 206	. . . . . . . . . . . . . . 15 |- ((rank` (A X. B)) = (/) \/ E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B)))
31		3orass 861	. . . . . . . . . . . . . . 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 206	. . . . . . . . . . . . . 14 |- ((rank` (A X. B)) = (/) \/ (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
33	32	ori 247	. . . . . . . . . . . . 13 |- (-. (rank` (A X. B)) = (/) -> (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
34	26, 33	sylbi 216	. . . . . . . . . . . 12 |- ((A X. B) =/= (/) -> (E.x e. On (rank` (A X. B)) = suc x \/ Lim (rank` (A X. B))))
35	34	ord 249	. . . . . . . . . . 11 |- ((A X. B) =/= (/) -> (-. E.x e. On (rank` (A X. B)) = suc x -> Lim (rank` (A X. B))))
36	35	con1d 109	. . . . . . . . . 10 |- ((A X. B) =/= (/) -> (-. Lim (rank` (A X. B)) -> E.x e. On (rank` (A X. B)) = suc x))
37	36	com12 14	. . . . . . . . 9 |- (-. Lim (rank` (A X. B)) -> ((A X. B) =/= (/) -> E.x e. On (rank` (A X. B)) = suc x))
38	19, 23, 37	3syl 24	. . . . . . . 8 |- ((rank` (A u. B)) = suc C -> ((A X. B) =/= (/) -> E.x e. On (rank` (A X. B)) = suc x))
39		visset 2295	. . . . . . . . . . . . 13 |- x e. _V
40		nlimsucg 3923	. . . . . . . . . . . . 13 |- (x e. _V -> -. Lim suc x)
41	39, 40	ax-mp 7	. . . . . . . . . . . 12 |- -. Lim suc x
42		limeq 3669	. . . . . . . . . . . 12 |- ((rank` (A X. B)) = suc x -> (Lim (rank` (A X. B)) <-> Lim suc x))
43	41, 42	mtbiri 785	. . . . . . . . . . 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 2211	. . . . . . . . 9 |- (E.x e. On (rank` (A X. B)) = suc x -> -. Lim (rank` (A X. B)))
46	20, 21	rankxplim3 5825	. . . . . . . . . 10 |- (Lim (rank` (A X. B)) <-> Lim U.(rank` (A X. B)))
47	46	notbii 204	. . . . . . . . 9 |- (-. Lim (rank` (A X. B)) <-> -. Lim U.(rank` (A X. B)))
48	45, 47	sylib 215	. . . . . . . 8 |- (E.x e. On (rank` (A X. B)) = suc x -> -. Lim U.(rank` (A X. B)))
49	38, 48	syl6com 64	. . . . . . 7 |- ((A X. B) =/= (/) -> ((rank` (A u. B)) = suc C -> -. Lim U.(rank` (A X. B))))
50		unixp0 4423	. . . . . . . . . . . 12 |- ((A X. B) = (/) <-> U.(A X. B) = (/))
51	24	uniex 3794	. . . . . . . . . . . . 13 |- U.(A X. B) e. _V
52	51	rankeq0 5807	. . . . . . . . . . . 12 |- (U.(A X. B) = (/) <-> (rank` U.(A X. B)) = (/))
53	4	eqeq1i 1891	. . . . . . . . . . . 12 |- ((rank` U.(A X. B)) = (/) <-> U.(rank` (A X. B)) = (/))
54	50, 52, 53	3bitri 194	. . . . . . . . . . 11 |- ((A X. B) = (/) <-> U.(rank` (A X. B)) = (/))
55	54	necon3abii 2030	. . . . . . . . . 10 |- ((A X. B) =/= (/) <-> -. U.(rank` (A X. B)) = (/))
56		onuni 3874	. . . . . . . . . . . . . . 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	onordi 3774	. . . . . . . . . . . . 13 |- Ord U.(rank` (A X. B))
59		ordzsl 3927	. . . . . . . . . . . . 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 206	. . . . . . . . . . . 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 861	. . . . . . . . . . . 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 206	. . . . . . . . . . 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 247	. . . . . . . . . 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 216	. . . . . . . . 9 |- ((A X. B) =/= (/) -> (E.x e. On U.(rank` (A X. B)) = suc x \/ Lim U.(rank` (A X. B))))
65	64	ord 249	. . . . . . . 8 |- ((A X. B) =/= (/) -> (-. E.x e. On U.(rank` (A X. B)) = suc x -> Lim U.(rank` (A X. B))))
66	65	con1d 109	. . . . . . 7 |- ((A X. B) =/= (/) -> (-. Lim U.(rank` (A X. B)) -> E.x e. On U.(rank` (A X. B)) = suc x))
67	49, 66	syld 30	. . . . . 6 |- ((A X. B) =/= (/) -> ((rank` (A u. B)) = suc C -> E.x e. On U.(rank` (A X. B)) = suc x))
68	67	impcom 378	. . . . 5 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> E.x e. On U.(rank` (A X. B)) = suc x)
69		onsucuni2 3914	. . . . . . . 8 |- ((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)))
70	57, 69	mpan 759	. . . . . . 7 |- (U.(rank` (A X. B)) = suc x -> suc U.U.(rank` (A X. B)) = U.(rank` (A X. B)))
71	70	a1i 8	. . . . . 6 |- (x e. On -> (U.(rank` (A X. B)) = suc x -> suc U.U.(rank` (A X. B)) = U.(rank` (A X. B))))
72	71	r19.23aiv 2211	. . . . 5 |- (E.x e. On U.(rank` (A X. B)) = suc x -> suc U.U.(rank` (A X. B)) = U.(rank` (A X. B)))
73	68, 72	syl 12	. . . 4 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc U.U.(rank` (A X. B)) = U.(rank` (A X. B)))
74	10, 73	eqtrd 1925	. . 3 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc (rank` (A u. B)) = U.(rank` (A X. B)))
75		suc11reg 5710	. . 3 |- (suc suc (rank` (A u. B)) = suc U.(rank` (A X. B)) <-> suc (rank` (A u. B)) = U.(rank` (A X. B)))
76	74, 75	sylibr 217	. 2 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc suc (rank` (A u. B)) = suc U.(rank` (A X. B)))
77	38	imp 377	. . 3 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> E.x e. On (rank` (A X. B)) = suc x)
78		onsucuni2 3914	. . . . . 6 |- (((rank` (A X. B)) e. On /\ (rank` (A X. B)) = suc x) -> suc U.(rank` (A X. B)) = (rank` (A X. B)))
79	27, 78	mpan 759	. . . . 5 |- ((rank` (A X. B)) = suc x -> suc U.(rank` (A X. B)) = (rank` (A X. B)))
80	79	a1i 8	. . . 4 |- (x e. On -> ((rank` (A X. B)) = suc x -> suc U.(rank` (A X. B)) = (rank` (A X. B))))
81	80	r19.23aiv 2211	. . 3 |- (E.x e. On (rank` (A X. B)) = suc x -> suc U.(rank` (A X. B)) = (rank` (A X. B)))
82	77, 81	syl 12	. 2 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> suc U.(rank` (A X. B)) = (rank` (A X. B)))
83	76, 82	eqtr2d 1926	1 |- (((rank` (A u. B)) = suc C /\ (A X. B) =/= (/)) -> (rank` (A X. B)) = suc suc (rank` (A u. B)))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300   =/= wne 2017  E.wrex 2106  _Vcvv 2292   u. cun 2591  (/)c0 2875  U.cuni 3177  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659   X. cxp 3984  ` cfv 3998  rankcrnk 5749

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-rdg 5140  df-r1 5750  df-rank 5751

Copyright terms: Public domain