rankxplim3 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rankxplim3		Structured version Unicode version

Theorem rankxplim3 8080

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 4775	. 2
2		0ellim 4776	. . . 4
3		n0i 3637	. . . 4
4		unieq 4094	. . . . . 6
5		uni0 4113	. . . . . 6
6	4, 5	syl6eq 2486	. . . . 5
7	6	con3i 135	. . . 4
8	2, 3, 7	3syl 20	. . 3
9		rankon 7994	. . . . . . . . . 10
10	9	onsuci 6444	. . . . . . . . 9
11	10	onsuci 6444	. . . . . . . 8
12	11	elexi 2977	. . . . . . 7
13	12	sucid 4793	. . . . . 6
14	11	onsuci 6444	. . . . . . . 8
15		ontri1 4748	. . . . . . . 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 8075	. . . . . 6
22		sstr 3359	. . . . . 6 $/\$
23	21, 22	mpan2 671	. . . . 5
24	18, 23	mto 176	. . . 4
25		reeanv 2883	. . . . 5 $/\$ $/\$
26		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$
27		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
28		rankuni 8062	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 8062	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 4095	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2458	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2603	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 6503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 8060	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 250	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 196	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5365	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2485	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3403	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
45	27, 44	eqsstr3d 3386	. . . . . . . . . . . . . . . . 17 $/\$
46	45	adantrr 716	. . . . . . . . . . . . . . . 16 $/\$ $/\$
47		limuni 4774	. . . . . . . . . . . . . . . . 17
48	47	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49	46, 48	sseqtr4d 3388	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		vex 2970	. . . . . . . . . . . . . . . 16
51		rankon 7994	. . . . . . . . . . . . . . . . . 18
52	51	onordi 4818	. . . . . . . . . . . . . . . . 17
53		orduni 6400	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . 16
55		ordelsuc 6426	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	mp2an 672	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$
58		limsuc 6455	. . . . . . . . . . . . . . 15
59	58	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$
60	57, 59	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$
61	26, 60	eqeltrd 2512	. . . . . . . . . . . 12 $/\$ $/\$
62		limsuc 6455	. . . . . . . . . . . . 13
63	62	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
64	61, 63	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
65		ordsucelsuc 6428	. . . . . . . . . . . 12
66	54, 65	ax-mp 5	. . . . . . . . . . 11
67	64, 66	sylib 196	. . . . . . . . . 10 $/\$ $/\$
68		onsucuni2 6440	. . . . . . . . . . . 12 $/\$
69	51, 68	mpan 670	. . . . . . . . . . 11
70	69	ad2antll 728	. . . . . . . . . 10 $/\$ $/\$
71	67, 70	eleqtrd 2514	. . . . . . . . 9 $/\$ $/\$
72	11, 51	onsucssi 6447	. . . . . . . . 9
73	71, 72	sylib 196	. . . . . . . 8 $/\$ $/\$
74	73	ex 434	. . . . . . 7 $/\$
75	74	a1d 25	. . . . . 6 $/\$ $/\$
76	75	rexlimdvv 2842	. . . . 5 $/\$
77	25, 76	syl5bir 218	. . . 4 $/\$
78	24, 77	mtoi 178	. . 3 $/\$
79		ianor 488	. . . . . 6 $/\$ $\/$
80		un00 3709	. . . . . . . . . . . . . 14 $/\$
81		olc 384	. . . . . . . . . . . . . . 15 $\/$
82	81	adantl 466	. . . . . . . . . . . . . 14 $/\$ $\/$
83	80, 82	sylbir 213	. . . . . . . . . . . . 13 $\/$
84		xpeq0 5253	. . . . . . . . . . . . 13 $\/$
85	83, 84	sylibr 212	. . . . . . . . . . . 12
86	85	con3i 135	. . . . . . . . . . 11
87	35, 86	sylbir 213	. . . . . . . . . 10
88	19, 20	unex 6373	. . . . . . . . . . . 12
89	88	rankeq0 8060	. . . . . . . . . . 11
90	89	notbii 296	. . . . . . . . . 10
91	87, 90	sylib 196	. . . . . . . . 9
92	9	onordi 4818	. . . . . . . . . . 11
93		ordzsl 6451	. . . . . . . . . . 11 $\/$ $\/$
94	92, 93	mpbi 208	. . . . . . . . . 10 $\/$ $\/$
95	94	3ori 1278	. . . . . . . . 9 $/\$
96	91, 95	sylan 471	. . . . . . . 8 $/\$
97	96	ex 434	. . . . . . 7
98		ordzsl 6451	. . . . . . . . . 10 $\/$ $\/$
99	52, 98	mpbi 208	. . . . . . . . 9 $\/$ $\/$
100	99	3ori 1278	. . . . . . . 8 $/\$
101	100	ex 434	. . . . . . 7
102	97, 101	orim12d 834	. . . . . 6 $\/$ $\/$
103	79, 102	syl5bi 217	. . . . 5 $/\$ $\/$
104	103	imp 429	. . . 4 $/\$ $/\$ $\/$
105		simpl 457	. . . . . . . 8 $/\$
106	34	necon3abii 2633	. . . . . . . . . 10
107	19, 20	rankxplim 8078	. . . . . . . . . 10 $/\$
108	106, 107	sylan2br 476	. . . . . . . . 9 $/\$
109		limeq 4726	. . . . . . . . 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

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 964

wceq 1369

wcel 1756

wne 2601

wrex 2711

cvv 2967

cun 3321

wss 3323

c0 3632

cuni 4086

word 4713

con0 4714

wlim 4715

csuc 4716

cxp 4833

cfv 5413

crnk 7962

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-reg 7799 ax-inf2 7839

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-om 6472 df-recs 6824 df-rdg 6858 df-r1 7963 df-rank 7964

This theorem is referenced by: rankxpsuc 8081

W3C validator