Theorem rankxplim 5823

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

Hypotheses

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

Assertion

Ref	Expression
rankxplim	|- ((Lim (rank` (A u. B)) /\ (A X. B) =/= (/)) -> (rank` (A X. B)) = (rank` (A u. B)))

Proof of Theorem rankxplim

Step	Hyp	Ref	Expression
1		rankon 5782	. . . . . . . . 9 |- (rank` <.x, y>.) e. On
2		rankon 5782	. . . . . . . . 9 |- (rank` (A u. B)) e. On
3		ontr2 3711	. . . . . . . . 9 |- (((rank` <.x, y>.) e. On /\ (rank` (A u. B)) e. On) -> (((rank` <.x, y>.) C_ (rank` ~P~P(x u. y)) /\ (rank` ~P~P(x u. y)) e. (rank` (A u. B))) -> (rank` <.x, y>.) e. (rank` (A u. B))))
4	1, 2, 3	mp2an 761	. . . . . . . 8 |- (((rank` <.x, y>.) C_ (rank` ~P~P(x u. y)) /\ (rank` ~P~P(x u. y)) e. (rank` (A u. B))) -> (rank` <.x, y>.) e. (rank` (A u. B)))
5		pwuni 3505	. . . . . . . . . . 11 |- <.x, y>. C_ ~PU.<.x, y>.
6		uniop 3555	. . . . . . . . . . . 12 |- U.<.x, y>. = {x, y}
7		pweq 3036	. . . . . . . . . . . 12 |- (U.<.x, y>. = {x, y} -> ~PU.<.x, y>. = ~P{x, y})
8	6, 7	ax-mp 7	. . . . . . . . . . 11 |- ~PU.<.x, y>. = ~P{x, y}
9	5, 8	sseqtri 2649	. . . . . . . . . 10 |- <.x, y>. C_ ~P{x, y}
10		pwuni 3505	. . . . . . . . . . . 12 |- {x, y} C_ ~PU.{x, y}
11		visset 2295	. . . . . . . . . . . . . 14 |- x e. _V
12		visset 2295	. . . . . . . . . . . . . 14 |- y e. _V
13	11, 12	unipr 3191	. . . . . . . . . . . . 13 |- U.{x, y} = (x u. y)
14		pweq 3036	. . . . . . . . . . . . 13 |- (U.{x, y} = (x u. y) -> ~PU.{x, y} = ~P(x u. y))
15	13, 14	ax-mp 7	. . . . . . . . . . . 12 |- ~PU.{x, y} = ~P(x u. y)
16	10, 15	sseqtri 2649	. . . . . . . . . . 11 |- {x, y} C_ ~P(x u. y)
17		sspwb 3503	. . . . . . . . . . 11 |- ({x, y} C_ ~P(x u. y) <-> ~P{x, y} C_ ~P~P(x u. y))
18	16, 17	mpbi 206	. . . . . . . . . 10 |- ~P{x, y} C_ ~P~P(x u. y)
19	9, 18	sstri 2626	. . . . . . . . 9 |- <.x, y>. C_ ~P~P(x u. y)
20	11, 12	unex 3796	. . . . . . . . . . . 12 |- (x u. y) e. _V
21	20	pwex 3487	. . . . . . . . . . 11 |- ~P(x u. y) e. _V
22	21	pwex 3487	. . . . . . . . . 10 |- ~P~P(x u. y) e. _V
23	22	rankss 5799	. . . . . . . . 9 |- (<.x, y>. C_ ~P~P(x u. y) -> (rank` <.x, y>.) C_ (rank` ~P~P(x u. y)))
24	19, 23	ax-mp 7	. . . . . . . 8 |- (rank` <.x, y>.) C_ (rank` ~P~P(x u. y))
25		rankxplim.1	. . . . . . . . . . . 12 |- A e. _V
26		rankxplim.2	. . . . . . . . . . . 12 |- B e. _V
27	11, 12, 25, 26	rankelun 5818	. . . . . . . . . . 11 |- (((rank` x) e. (rank` A) /\ (rank` y) e. (rank` B)) -> (rank` (x u. y)) e. (rank` (A u. B)))
28	25	rankel 5791	. . . . . . . . . . 11 |- (x e. A -> (rank` x) e. (rank` A))
29	26	rankel 5791	. . . . . . . . . . 11 |- (y e. B -> (rank` y) e. (rank` B))
30	27, 28, 29	syl2an 503	. . . . . . . . . 10 |- ((x e. A /\ y e. B) -> (rank` (x u. y)) e. (rank` (A u. B)))
31	30	adantl 424	. . . . . . . . 9 |- ((Lim (rank` (A u. B)) /\ (x e. A /\ y e. B)) -> (rank` (x u. y)) e. (rank` (A u. B)))
32		ranklim 5796	. . . . . . . . . . 11 |- (Lim (rank` (A u. B)) -> ((rank` (x u. y)) e. (rank` (A u. B)) <-> (rank` ~P(x u. y)) e. (rank` (A u. B))))
33		ranklim 5796	. . . . . . . . . . 11 |- (Lim (rank` (A u. B)) -> ((rank` ~P(x u. y)) e. (rank` (A u. B)) <-> (rank` ~P~P(x u. y)) e. (rank` (A u. B))))
34	32, 33	bitrd 587	. . . . . . . . . 10 |- (Lim (rank` (A u. B)) -> ((rank` (x u. y)) e. (rank` (A u. B)) <-> (rank` ~P~P(x u. y)) e. (rank` (A u. B))))
35	34	adantr 425	. . . . . . . . 9 |- ((Lim (rank` (A u. B)) /\ (x e. A /\ y e. B)) -> ((rank` (x u. y)) e. (rank` (A u. B)) <-> (rank` ~P~P(x u. y)) e. (rank` (A u. B))))
36	31, 35	mpbid 212	. . . . . . . 8 |- ((Lim (rank` (A u. B)) /\ (x e. A /\ y e. B)) -> (rank` ~P~P(x u. y)) e. (rank` (A u. B)))
37	4, 24, 36	sylancr 526	. . . . . . 7 |- ((Lim (rank` (A u. B)) /\ (x e. A /\ y e. B)) -> (rank` <.x, y>.) e. (rank` (A u. B)))
38	1, 2	onsucssi 3922	. . . . . . 7 |- ((rank` <.x, y>.) e. (rank` (A u. B)) <-> suc (rank` <.x, y>.) C_ (rank` (A u. B)))
39	37, 38	sylib 215	. . . . . 6 |- ((Lim (rank` (A u. B)) /\ (x e. A /\ y e. B)) -> suc (rank` <.x, y>.) C_ (rank` (A u. B)))
40	39	ex 402	. . . . 5 |- (Lim (rank` (A u. B)) -> ((x e. A /\ y e. B) -> suc (rank` <.x, y>.) C_ (rank` (A u. B))))
41	40	r19.21aivv 2183	. . . 4 |- (Lim (rank` (A u. B)) -> A.x e. A A.y e. B suc (rank` <.x, y>.) C_ (rank` (A u. B)))
42		fveq2 4681	. . . . . . . 8 |- (z = <.x, y>. -> (rank` z) = (rank` <.x, y>.))
43		suceq 3729	. . . . . . . 8 |- ((rank` z) = (rank` <.x, y>.) -> suc (rank` z) = suc (rank` <.x, y>.))
44	42, 43	syl 12	. . . . . . 7 |- (z = <.x, y>. -> suc (rank` z) = suc (rank` <.x, y>.))
45	44	sseq1d 2644	. . . . . 6 |- (z = <.x, y>. -> (suc (rank` z) C_ (rank` (A u. B)) <-> suc (rank` <.x, y>.) C_ (rank` (A u. B))))
46	45	ralxp 4041	. . . . 5 |- (A.z e. (A X. B)suc (rank` z) C_ (rank` (A u. B)) <-> A.x e. A A.y e. B suc (rank` <.x, y>.) C_ (rank` (A u. B)))
47	25, 26	xpex 4096	. . . . . 6 |- (A X. B) e. _V
48	47	rankbnd 5814	. . . . 5 |- (A.z e. (A X. B)suc (rank` z) C_ (rank` (A u. B)) <-> (rank` (A X. B)) C_ (rank` (A u. B)))
49	46, 48	bitr3i 192	. . . 4 |- (A.x e. A A.y e. B suc (rank` <.x, y>.) C_ (rank` (A u. B)) <-> (rank` (A X. B)) C_ (rank` (A u. B)))
50	41, 49	sylib 215	. . 3 |- (Lim (rank` (A u. B)) -> (rank` (A X. B)) C_ (rank` (A u. B)))
51	50	adantr 425	. 2 |- ((Lim (rank` (A u. B)) /\ (A X. B) =/= (/)) -> (rank` (A X. B)) C_ (rank` (A u. B)))
52	25, 26	rankxpl 5821	. . 3 |- ((A X. B) =/= (/) -> (rank` (A u. B)) C_ (rank` (A X. B)))
53	52	adantl 424	. 2 |- ((Lim (rank` (A u. B)) /\ (A X. B) =/= (/)) -> (rank` (A u. B)) C_ (rank` (A X. B)))
54	51, 53	eqssd 2633	1 |- ((Lim (rank` (A u. B)) /\ (A X. B) =/= (/)) -> (rank` (A X. B)) = (rank` (A u. B)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {cpr 3045  <.cop 3046  U.cuni 3177  Oncon0 3657  Lim wlim 3658  suc csuc 3659   X. cxp 3984  ` cfv 3998  rankcrnk 5749

This theorem is referenced by:  rankxplim3 5825

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