Theorem rankxplim3 8320

Description: The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006.)

Hypotheses

Ref	Expression
rankxplim.1
rankxplim.2

Assertion

Ref	Expression
rankxplim3

Proof of Theorem rankxplim3

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limuni2 4944	. 2
2		0ellim 4945	. . . 4
3		n0i 3789	. . . 4
4		unieq 4257	. . . . . 6
5		uni0 4276	. . . . . 6
6	4, 5	syl6eq 2514	. . . . 5
7	6	con3i 135	. . . 4
8	2, 3, 7	3syl 20	. . 3
9		rankon 8234	. . . . . . . . . 10
10	9	onsuci 6673	. . . . . . . . 9
11	10	onsuci 6673	. . . . . . . 8
12	11	elexi 3119	. . . . . . 7
13	12	sucid 4962	. . . . . 6
14	11	onsuci 6673	. . . . . . . 8
15		ontri1 4917	. . . . . . . 8
16	14, 11, 15	mp2an 672	. . . . . . 7
17	16	con2bii 332	. . . . . 6
18	13, 17	mpbi 208	. . . . 5
19		rankxplim.1	. . . . . . 7
20		rankxplim.2	. . . . . . 7
21	19, 20	rankxpu 8315	. . . . . 6
22		sstr 3511	. . . . . 6
23	21, 22	mpan2 671	. . . . 5
24	18, 23	mto 176	. . . 4
25		reeanv 3025	. . . . 5
26		simprl 756	. . . . . . . . . . . . 13
27		simpr 461	. . . . . . . . . . . . . . . . . 18
28		rankuni 8302	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 8302	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 4258	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2486	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2654	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 6604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 8300	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 250	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 196	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5545	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5875	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2513	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3555	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 465	. . . . . . . . . . . . . . . . . 18
45	27, 44	eqsstr3d 3538	. . . . . . . . . . . . . . . . 17
46	45	adantrr 716	. . . . . . . . . . . . . . . 16
47		limuni 4943	. . . . . . . . . . . . . . . . 17
48	47	adantr 465	. . . . . . . . . . . . . . . 16
49	46, 48	sseqtr4d 3540	. . . . . . . . . . . . . . 15
50		vex 3112	. . . . . . . . . . . . . . . 16
51		rankon 8234	. . . . . . . . . . . . . . . . . 18
52	51	onordi 4987	. . . . . . . . . . . . . . . . 17
53		orduni 6629	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . 16
55		ordelsuc 6655	. . . . . . . . . . . . . . . 16
56	50, 54, 55	mp2an 672	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 212	. . . . . . . . . . . . . 14
58		limsuc 6684	. . . . . . . . . . . . . . 15
59	58	adantr 465	. . . . . . . . . . . . . 14
60	57, 59	mpbid 210	. . . . . . . . . . . . 13
61	26, 60	eqeltrd 2545	. . . . . . . . . . . 12
62		limsuc 6684	. . . . . . . . . . . . 13
63	62	adantr 465	. . . . . . . . . . . 12
64	61, 63	mpbid 210	. . . . . . . . . . 11
65		ordsucelsuc 6657	. . . . . . . . . . . 12
66	54, 65	ax-mp 5	. . . . . . . . . . 11
67	64, 66	sylib 196	. . . . . . . . . 10
68		onsucuni2 6669	. . . . . . . . . . . 12
69	51, 68	mpan 670	. . . . . . . . . . 11
70	69	ad2antll 728	. . . . . . . . . 10
71	67, 70	eleqtrd 2547	. . . . . . . . 9
72	11, 51	onsucssi 6676	. . . . . . . . 9
73	71, 72	sylib 196	. . . . . . . 8
74	73	ex 434	. . . . . . 7
75	74	a1d 25	. . . . . 6
76	75	rexlimdvv 2955	. . . . 5
77	25, 76	syl5bir 218	. . . 4
78	24, 77	mtoi 178	. . 3
79		ianor 488	. . . . . 6
80		un00 3862	. . . . . . . . . . . . . 14
81		olc 384	. . . . . . . . . . . . . . 15
82	81	adantl 466	. . . . . . . . . . . . . 14
83	80, 82	sylbir 213	. . . . . . . . . . . . 13
84		xpeq0 5432	. . . . . . . . . . . . 13
85	83, 84	sylibr 212	. . . . . . . . . . . 12
86	85	con3i 135	. . . . . . . . . . 11
87	35, 86	sylbir 213	. . . . . . . . . 10
88	19, 20	unex 6598	. . . . . . . . . . . 12
89	88	rankeq0 8300	. . . . . . . . . . 11
90	89	notbii 296	. . . . . . . . . 10
91	87, 90	sylib 196	. . . . . . . . 9
92	9	onordi 4987	. . . . . . . . . . 11
93		ordzsl 6680	. . . . . . . . . . 11
94	92, 93	mpbi 208	. . . . . . . . . 10
95	94	3ori 1288	. . . . . . . . 9
96	91, 95	sylan 471	. . . . . . . 8
97	96	ex 434	. . . . . . 7
98		ordzsl 6680	. . . . . . . . . 10
99	52, 98	mpbi 208	. . . . . . . . 9
100	99	3ori 1288	. . . . . . . 8
101	100	ex 434	. . . . . . 7
102	97, 101	orim12d 838	. . . . . 6
103	79, 102	syl5bi 217	. . . . 5
104	103	imp 429	. . . 4
105		simpl 457	. . . . . . . 8
106	34	necon3abii 2717	. . . . . . . . . 10
107	19, 20	rankxplim 8318	. . . . . . . . . 10
108	106, 107	sylan2br 476	. . . . . . . . 9
109		limeq 4895	. . . . . . . . 9
110	108, 109	syl 16	. . . . . . . 8
111	105, 110	mpbird 232	. . . . . . 7
112	111	expcom 435	. . . . . 6
113		idd 24	. . . . . 6
114	112, 113	jaod 380	. . . . 5
115	114	adantr 465	. . . 4
116	104, 115	mpd 15	. . 3
117	8, 78, 116	syl2anc 661	. 2
118	1, 117	impbii 188	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/w3o 972  =wceq 1395  e.wcel 1818  =/=wne 2652  E.wrex 2808  cvv 3109  u.cun 3473  C_wss 3475  c0 3784  U.cuni 4249  Ordword 4882  con0 4883  Limwlim 4884  succsuc 4885  X.cxp 5002  `cfv 5593  crnk 8202

This theorem is referenced by:  rankxpsuc  8321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-reg 8039  ax-inf2 8079

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-om 6701  df-recs 7061  df-rdg 7095  df-r1 8203  df-rank 8204