rankxplim3 - Metamath Proof Explorer

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

Theorem rankxplim3 8192

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 4881	. 2
2		0ellim 4882	. . . 4
3		n0i 3743	. . . 4
4		unieq 4200	. . . . . 6
5		uni0 4219	. . . . . 6
6	4, 5	syl6eq 2508	. . . . 5
7	6	con3i 135	. . . 4
8	2, 3, 7	3syl 20	. . 3
9		rankon 8106	. . . . . . . . . 10
10	9	onsuci 6552	. . . . . . . . 9
11	10	onsuci 6552	. . . . . . . 8
12	11	elexi 3081	. . . . . . 7
13	12	sucid 4899	. . . . . 6
14	11	onsuci 6552	. . . . . . . 8
15		ontri1 4854	. . . . . . . 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 8187	. . . . . 6
22		sstr 3465	. . . . . 6 $/\$
23	21, 22	mpan2 671	. . . . 5
24	18, 23	mto 176	. . . 4
25		reeanv 2987	. . . . 5 $/\$ $/\$
26		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$
27		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
28		rankuni 8174	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 8174	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 4201	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2480	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2646	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 6611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 8172	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 250	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 196	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5471	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5796	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2507	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3509	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
45	27, 44	eqsstr3d 3492	. . . . . . . . . . . . . . . . 17 $/\$
46	45	adantrr 716	. . . . . . . . . . . . . . . 16 $/\$ $/\$
47		limuni 4880	. . . . . . . . . . . . . . . . 17
48	47	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49	46, 48	sseqtr4d 3494	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		vex 3074	. . . . . . . . . . . . . . . 16
51		rankon 8106	. . . . . . . . . . . . . . . . . 18
52	51	onordi 4924	. . . . . . . . . . . . . . . . 17
53		orduni 6508	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . 16
55		ordelsuc 6534	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	mp2an 672	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$
58		limsuc 6563	. . . . . . . . . . . . . . 15
59	58	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$
60	57, 59	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$
61	26, 60	eqeltrd 2539	. . . . . . . . . . . 12 $/\$ $/\$
62		limsuc 6563	. . . . . . . . . . . . 13
63	62	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
64	61, 63	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
65		ordsucelsuc 6536	. . . . . . . . . . . 12
66	54, 65	ax-mp 5	. . . . . . . . . . 11
67	64, 66	sylib 196	. . . . . . . . . 10 $/\$ $/\$
68		onsucuni2 6548	. . . . . . . . . . . 12 $/\$
69	51, 68	mpan 670	. . . . . . . . . . 11
70	69	ad2antll 728	. . . . . . . . . 10 $/\$ $/\$
71	67, 70	eleqtrd 2541	. . . . . . . . 9 $/\$ $/\$
72	11, 51	onsucssi 6555	. . . . . . . . 9
73	71, 72	sylib 196	. . . . . . . 8 $/\$ $/\$
74	73	ex 434	. . . . . . 7 $/\$
75	74	a1d 25	. . . . . 6 $/\$ $/\$
76	75	rexlimdvv 2946	. . . . 5 $/\$
77	25, 76	syl5bir 218	. . . 4 $/\$
78	24, 77	mtoi 178	. . 3 $/\$
79		ianor 488	. . . . . 6 $/\$ $\/$
80		un00 3815	. . . . . . . . . . . . . 14 $/\$
81		olc 384	. . . . . . . . . . . . . . 15 $\/$
82	81	adantl 466	. . . . . . . . . . . . . 14 $/\$ $\/$
83	80, 82	sylbir 213	. . . . . . . . . . . . 13 $\/$
84		xpeq0 5359	. . . . . . . . . . . . 13 $\/$
85	83, 84	sylibr 212	. . . . . . . . . . . 12
86	85	con3i 135	. . . . . . . . . . 11
87	35, 86	sylbir 213	. . . . . . . . . 10
88	19, 20	unex 6481	. . . . . . . . . . . 12
89	88	rankeq0 8172	. . . . . . . . . . 11
90	89	notbii 296	. . . . . . . . . 10
91	87, 90	sylib 196	. . . . . . . . 9
92	9	onordi 4924	. . . . . . . . . . 11
93		ordzsl 6559	. . . . . . . . . . 11 $\/$ $\/$
94	92, 93	mpbi 208	. . . . . . . . . 10 $\/$ $\/$
95	94	3ori 1279	. . . . . . . . 9 $/\$
96	91, 95	sylan 471	. . . . . . . 8 $/\$
97	96	ex 434	. . . . . . 7
98		ordzsl 6559	. . . . . . . . . 10 $\/$ $\/$
99	52, 98	mpbi 208	. . . . . . . . 9 $\/$ $\/$
100	99	3ori 1279	. . . . . . . 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 2708	. . . . . . . . . 10
107	19, 20	rankxplim 8190	. . . . . . . . . 10 $/\$
108	106, 107	sylan2br 476	. . . . . . . . 9 $/\$
109		limeq 4832	. . . . . . . . 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 1370

wcel 1758

wne 2644

wrex 2796

cvv 3071

cun 3427

wss 3429

c0 3738

cuni 4192

word 4819

con0 4820

wlim 4821

csuc 4822

cxp 4939

cfv 5519

crnk 8074

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-reg 7911 ax-inf2 7951

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-om 6580 df-recs 6935 df-rdg 6969 df-r1 8075 df-rank 8076

This theorem is referenced by: rankxpsuc 8193

W3C validator