rankxplim3 - Metamath Proof Explorer

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

Theorem rankxplim3 8355

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 5501	. 2
2		0ellim 5502	. . . 4
3		n0i 3767	. . . 4
4		unieq 4225	. . . . . 6
5		uni0 4244	. . . . . 6
6	4, 5	syl6eq 2480	. . . . 5
7	6	con3i 141	. . . 4
8	2, 3, 7	3syl 18	. . 3
9		rankon 8269	. . . . . . . . . 10
10	9	onsuci 6677	. . . . . . . . 9
11	10	onsuci 6677	. . . . . . . 8
12	11	elexi 3092	. . . . . . 7
13	12	sucid 5519	. . . . . 6
14	11	onsuci 6677	. . . . . . . 8
15		ontri1 5474	. . . . . . . 8 $/\$
16	14, 11, 15	mp2an 677	. . . . . . 7
17	16	con2bii 334	. . . . . 6
18	13, 17	mpbi 212	. . . . 5
19		rankxplim.1	. . . . . . 7
20		rankxplim.2	. . . . . . 7
21	19, 20	rankxpu 8350	. . . . . 6
22		sstr 3473	. . . . . 6 $/\$
23	21, 22	mpan2 676	. . . . 5
24	18, 23	mto 180	. . . 4
25		reeanv 2997	. . . . 5 $/\$ $/\$
26		simprl 763	. . . . . . . . . . . . 13 $/\$ $/\$
27		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$
28		rankuni 8337	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 8337	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 4226	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2452	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2621	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 6607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 8335	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 298	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 254	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 200	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5386	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2479	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3517	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
45	27, 44	eqsstr3d 3500	. . . . . . . . . . . . . . . . 17 $/\$
46	45	adantrr 722	. . . . . . . . . . . . . . . 16 $/\$ $/\$
47		limuni 5500	. . . . . . . . . . . . . . . . 17
48	47	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49	46, 48	sseqtr4d 3502	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		vex 3085	. . . . . . . . . . . . . . . 16
51		rankon 8269	. . . . . . . . . . . . . . . . . 18
52	51	onordi 5544	. . . . . . . . . . . . . . . . 17
53		orduni 6633	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . 16
55		ordelsuc 6659	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	mp2an 677	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$
58		limsuc 6688	. . . . . . . . . . . . . . 15
59	58	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$
60	57, 59	mpbid 214	. . . . . . . . . . . . 13 $/\$ $/\$
61	26, 60	eqeltrd 2511	. . . . . . . . . . . 12 $/\$ $/\$
62		limsuc 6688	. . . . . . . . . . . . 13
63	62	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$
64	61, 63	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$
65		ordsucelsuc 6661	. . . . . . . . . . . 12
66	54, 65	ax-mp 5	. . . . . . . . . . 11
67	64, 66	sylib 200	. . . . . . . . . 10 $/\$ $/\$
68		onsucuni2 6673	. . . . . . . . . . . 12 $/\$
69	51, 68	mpan 675	. . . . . . . . . . 11
70	69	ad2antll 734	. . . . . . . . . 10 $/\$ $/\$
71	67, 70	eleqtrd 2513	. . . . . . . . 9 $/\$ $/\$
72	11, 51	onsucssi 6680	. . . . . . . . 9
73	71, 72	sylib 200	. . . . . . . 8 $/\$ $/\$
74	73	ex 436	. . . . . . 7 $/\$
75	74	a1d 27	. . . . . 6 $/\$ $/\$
76	75	rexlimdvv 2924	. . . . 5 $/\$
77	25, 76	syl5bir 222	. . . 4 $/\$
78	24, 77	mtoi 182	. . 3 $/\$
79		ianor 491	. . . . . 6 $/\$ $\/$
80		un00 3829	. . . . . . . . . . . . . 14 $/\$
81		olc 386	. . . . . . . . . . . . . . 15 $\/$
82	81	adantl 468	. . . . . . . . . . . . . 14 $/\$ $\/$
83	80, 82	sylbir 217	. . . . . . . . . . . . 13 $\/$
84		xpeq0 5274	. . . . . . . . . . . . 13 $\/$
85	83, 84	sylibr 216	. . . . . . . . . . . 12
86	85	con3i 141	. . . . . . . . . . 11
87	35, 86	sylbir 217	. . . . . . . . . 10
88	19, 20	unex 6601	. . . . . . . . . . . 12
89	88	rankeq0 8335	. . . . . . . . . . 11
90	89	notbii 298	. . . . . . . . . 10
91	87, 90	sylib 200	. . . . . . . . 9
92	9	onordi 5544	. . . . . . . . . . 11
93		ordzsl 6684	. . . . . . . . . . 11 $\/$ $\/$
94	92, 93	mpbi 212	. . . . . . . . . 10 $\/$ $\/$
95	94	3ori 1325	. . . . . . . . 9 $/\$
96	91, 95	sylan 474	. . . . . . . 8 $/\$
97	96	ex 436	. . . . . . 7
98		ordzsl 6684	. . . . . . . . . 10 $\/$ $\/$
99	52, 98	mpbi 212	. . . . . . . . 9 $\/$ $\/$
100	99	3ori 1325	. . . . . . . 8 $/\$
101	100	ex 436	. . . . . . 7
102	97, 101	orim12d 847	. . . . . 6 $\/$ $\/$
103	79, 102	syl5bi 221	. . . . 5 $/\$ $\/$
104	103	imp 431	. . . 4 $/\$ $/\$ $\/$
105		simpl 459	. . . . . . . 8 $/\$
106	34	necon3abii 2685	. . . . . . . . . 10
107	19, 20	rankxplim 8353	. . . . . . . . . 10 $/\$
108	106, 107	sylan2br 479	. . . . . . . . 9 $/\$
109		limeq 5452	. . . . . . . . 9
110	108, 109	syl 17	. . . . . . . 8 $/\$
111	105, 110	mpbird 236	. . . . . . 7 $/\$
112	111	expcom 437	. . . . . 6
113		idd 26	. . . . . 6
114	112, 113	jaod 382	. . . . 5 $\/$
115	114	adantr 467	. . . 4 $/\$ $/\$ $\/$
116	104, 115	mpd 15	. . 3 $/\$ $/\$
117	8, 78, 116	syl2anc 666	. 2
118	1, 117	impbii 191	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $\/$ w3o 982

wceq 1438

wcel 1869

wne 2619

wrex 2777

cvv 3082

cun 3435

wss 3437

c0 3762

cuni 4217

cxp 4849

word 5439

con0 5440

wlim 5441

csuc 5442

cfv 5599

crnk 8237

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-reg 8111 ax-inf2 8150

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-ral 2781 df-rex 2782 df-reu 2783 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-om 6705 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-r1 8238 df-rank 8239

This theorem is referenced by: rankxpsuc 8356

W3C validator