rankxplim3 - Metamath Proof Explorer

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

Theorem rankxplim3 7761

Description: The rank of a cross 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 4602	. 2
2		0ellim 4603	. . . 4
3		n0i 3593	. . . 4
4		unieq 3984	. . . . . 6
5		uni0 4002	. . . . . 6
6	4, 5	syl6eq 2452	. . . . 5
7	6	con3i 129	. . . 4
8	2, 3, 7	3syl 19	. . 3
9		rankon 7677	. . . . . . . . . 10
10	9	onsuci 4777	. . . . . . . . 9
11	10	onsuci 4777	. . . . . . . 8
12	11	elexi 2925	. . . . . . 7
13	12	sucid 4620	. . . . . 6
14	11	onsuci 4777	. . . . . . . 8
15		ontri1 4575	. . . . . . . 8 $/\$
16	14, 11, 15	mp2an 654	. . . . . . 7
17	16	con2bii 323	. . . . . 6
18	13, 17	mpbi 200	. . . . 5
19		rankxplim.1	. . . . . . 7
20		rankxplim.2	. . . . . . 7
21	19, 20	rankxpu 7758	. . . . . 6
22		sstr 3316	. . . . . 6 $/\$
23	21, 22	mpan2 653	. . . . 5
24	18, 23	mto 169	. . . 4
25		reeanv 2835	. . . . 5 $/\$ $/\$
26		simprl 733	. . . . . . . . . . . . 13 $/\$ $/\$
27		simpr 448	. . . . . . . . . . . . . . . . . 18 $/\$
28		rankuni 7745	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 7745	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 3985	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2424	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2569	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 4949	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 7743	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 288	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 242	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 189	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5361	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2451	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3360	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$
45	27, 44	eqsstr3d 3343	. . . . . . . . . . . . . . . . 17 $/\$
46	45	adantrr 698	. . . . . . . . . . . . . . . 16 $/\$ $/\$
47		limuni 4601	. . . . . . . . . . . . . . . . 17
48	47	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49	46, 48	sseqtr4d 3345	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		vex 2919	. . . . . . . . . . . . . . . 16
51		rankon 7677	. . . . . . . . . . . . . . . . . 18
52	51	onordi 4645	. . . . . . . . . . . . . . . . 17
53		orduni 4733	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 8	. . . . . . . . . . . . . . . 16
55		ordelsuc 4759	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	mp2an 654	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 204	. . . . . . . . . . . . . 14 $/\$ $/\$
58		limsuc 4788	. . . . . . . . . . . . . . 15
59	58	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$
60	57, 59	mpbid 202	. . . . . . . . . . . . 13 $/\$ $/\$
61	26, 60	eqeltrd 2478	. . . . . . . . . . . 12 $/\$ $/\$
62		limsuc 4788	. . . . . . . . . . . . 13
63	62	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
64	61, 63	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$
65		ordsucelsuc 4761	. . . . . . . . . . . 12
66	54, 65	ax-mp 8	. . . . . . . . . . 11
67	64, 66	sylib 189	. . . . . . . . . 10 $/\$ $/\$
68		onsucuni2 4773	. . . . . . . . . . . 12 $/\$
69	51, 68	mpan 652	. . . . . . . . . . 11
70	69	ad2antll 710	. . . . . . . . . 10 $/\$ $/\$
71	67, 70	eleqtrd 2480	. . . . . . . . 9 $/\$ $/\$
72	11, 51	onsucssi 4780	. . . . . . . . 9
73	71, 72	sylib 189	. . . . . . . 8 $/\$ $/\$
74	73	ex 424	. . . . . . 7 $/\$
75	74	a1d 23	. . . . . 6 $/\$ $/\$
76	75	rexlimdvv 2796	. . . . 5 $/\$
77	25, 76	syl5bir 210	. . . 4 $/\$
78	24, 77	mtoi 171	. . 3 $/\$
79		ianor 475	. . . . . 6 $/\$ $\/$
80		un00 3623	. . . . . . . . . . . . . 14 $/\$
81		olc 374	. . . . . . . . . . . . . . 15 $\/$
82	81	adantl 453	. . . . . . . . . . . . . 14 $/\$ $\/$
83	80, 82	sylbir 205	. . . . . . . . . . . . 13 $\/$
84		xpeq0 5252	. . . . . . . . . . . . 13 $\/$
85	83, 84	sylibr 204	. . . . . . . . . . . 12
86	85	con3i 129	. . . . . . . . . . 11
87	35, 86	sylbir 205	. . . . . . . . . 10
88	19, 20	unex 4666	. . . . . . . . . . . 12
89	88	rankeq0 7743	. . . . . . . . . . 11
90	89	notbii 288	. . . . . . . . . 10
91	87, 90	sylib 189	. . . . . . . . 9
92	9	onordi 4645	. . . . . . . . . . 11
93		ordzsl 4784	. . . . . . . . . . 11 $\/$ $\/$
94	92, 93	mpbi 200	. . . . . . . . . 10 $\/$ $\/$
95	94	3ori 1244	. . . . . . . . 9 $/\$
96	91, 95	sylan 458	. . . . . . . 8 $/\$
97	96	ex 424	. . . . . . 7
98		ordzsl 4784	. . . . . . . . . 10 $\/$ $\/$
99	52, 98	mpbi 200	. . . . . . . . 9 $\/$ $\/$
100	99	3ori 1244	. . . . . . . 8 $/\$
101	100	ex 424	. . . . . . 7
102	97, 101	orim12d 812	. . . . . 6 $\/$ $\/$
103	79, 102	syl5bi 209	. . . . 5 $/\$ $\/$
104	103	imp 419	. . . 4 $/\$ $/\$ $\/$
105		simpl 444	. . . . . . . 8 $/\$
106	34	necon3abii 2597	. . . . . . . . . 10
107	19, 20	rankxplim 7759	. . . . . . . . . 10 $/\$
108	106, 107	sylan2br 463	. . . . . . . . 9 $/\$
109		limeq 4553	. . . . . . . . 9
110	108, 109	syl 16	. . . . . . . 8 $/\$
111	105, 110	mpbird 224	. . . . . . 7 $/\$
112	111	expcom 425	. . . . . 6
113		idd 22	. . . . . 6
114	112, 113	jaod 370	. . . . 5 $\/$
115	114	adantr 452	. . . 4 $/\$ $/\$ $\/$
116	104, 115	mpd 15	. . 3 $/\$ $/\$
117	8, 78, 116	syl2anc 643	. 2
118	1, 117	impbii 181	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $\/$ w3o 935

wceq 1649

wcel 1721

wne 2567

wrex 2667

cvv 2916

cun 3278

wss 3280

c0 3588

cuni 3975

word 4540

con0 4541

wlim 4542

csuc 4543

cxp 4835

cfv 5413

crnk 7645

This theorem is referenced by: rankxpsuc 7762

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-reg 7516 ax-inf2 7552

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-recs 6592 df-rdg 6627 df-r1 7646 df-rank 7647

W3C validator