rankxplim3 - Metamath Proof Explorer

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

Theorem rankxplim3 8316

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 4948	. 2
2		0ellim 4949	. . . 4
3		n0i 3798	. . . 4
4		unieq 4259	. . . . . 6
5		uni0 4278	. . . . . 6
6	4, 5	syl6eq 2514	. . . . 5
7	6	con3i 135	. . . 4
8	2, 3, 7	3syl 20	. . 3
9		rankon 8230	. . . . . . . . . 10
10	9	onsuci 6672	. . . . . . . . 9
11	10	onsuci 6672	. . . . . . . 8
12	11	elexi 3119	. . . . . . 7
13	12	sucid 4966	. . . . . 6
14	11	onsuci 6672	. . . . . . . 8
15		ontri1 4921	. . . . . . . 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 8311	. . . . . 6
22		sstr 3507	. . . . . 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 8298	. . . . . . . . . . . . . . . . . . . . . 22
29		rankuni 8298	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	unieqi 4260	. . . . . . . . . . . . . . . . . . . . . 22
31	28, 30	eqtri 2486	. . . . . . . . . . . . . . . . . . . . 21
32		df-ne 2654	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	19, 20	xpex 6603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34	33	rankeq0 8296	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	34	notbii 296	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	32, 35	bitr2i 250	. . . . . . . . . . . . . . . . . . . . . . . 24
37	8, 36	sylib 196	. . . . . . . . . . . . . . . . . . . . . . 23
38		unixp 5546	. . . . . . . . . . . . . . . . . . . . . . 23
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
40	39	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . 21
41	31, 40	syl5reqr 2513	. . . . . . . . . . . . . . . . . . . 20
42		eqimss 3551	. . . . . . . . . . . . . . . . . . . 20
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . 19
44	43	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
45	27, 44	eqsstr3d 3534	. . . . . . . . . . . . . . . . 17 $/\$
46	45	adantrr 716	. . . . . . . . . . . . . . . 16 $/\$ $/\$
47		limuni 4947	. . . . . . . . . . . . . . . . 17
48	47	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49	46, 48	sseqtr4d 3536	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		vex 3112	. . . . . . . . . . . . . . . 16
51		rankon 8230	. . . . . . . . . . . . . . . . . 18
52	51	onordi 4991	. . . . . . . . . . . . . . . . 17
53		orduni 6628	. . . . . . . . . . . . . . . . 17
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . 16
55		ordelsuc 6654	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	mp2an 672	. . . . . . . . . . . . . . 15
57	49, 56	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$
58		limsuc 6683	. . . . . . . . . . . . . . 15
59	58	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$
60	57, 59	mpbid 210	. . . . . . . . . . . . 13 $/\$ $/\$
61	26, 60	eqeltrd 2545	. . . . . . . . . . . 12 $/\$ $/\$
62		limsuc 6683	. . . . . . . . . . . . 13
63	62	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
64	61, 63	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
65		ordsucelsuc 6656	. . . . . . . . . . . 12
66	54, 65	ax-mp 5	. . . . . . . . . . 11
67	64, 66	sylib 196	. . . . . . . . . 10 $/\$ $/\$
68		onsucuni2 6668	. . . . . . . . . . . 12 $/\$
69	51, 68	mpan 670	. . . . . . . . . . 11
70	69	ad2antll 728	. . . . . . . . . 10 $/\$ $/\$
71	67, 70	eleqtrd 2547	. . . . . . . . 9 $/\$ $/\$
72	11, 51	onsucssi 6675	. . . . . . . . 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 3865	. . . . . . . . . . . . . 14 $/\$
81		olc 384	. . . . . . . . . . . . . . 15 $\/$
82	81	adantl 466	. . . . . . . . . . . . . 14 $/\$ $\/$
83	80, 82	sylbir 213	. . . . . . . . . . . . 13 $\/$
84		xpeq0 5434	. . . . . . . . . . . . 13 $\/$
85	83, 84	sylibr 212	. . . . . . . . . . . 12
86	85	con3i 135	. . . . . . . . . . 11
87	35, 86	sylbir 213	. . . . . . . . . 10
88	19, 20	unex 6597	. . . . . . . . . . . 12
89	88	rankeq0 8296	. . . . . . . . . . 11
90	89	notbii 296	. . . . . . . . . 10
91	87, 90	sylib 196	. . . . . . . . 9
92	9	onordi 4991	. . . . . . . . . . 11
93		ordzsl 6679	. . . . . . . . . . 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 6679	. . . . . . . . . 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 8314	. . . . . . . . . 10 $/\$
108	106, 107	sylan2br 476	. . . . . . . . 9 $/\$
109		limeq 4899	. . . . . . . . 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 972

wceq 1395

wcel 1819

wne 2652

wrex 2808

cvv 3109

cun 3469

wss 3471

c0 3793

cuni 4251

word 4886

con0 4887

wlim 4888

csuc 4889

cxp 5006

cfv 5594

crnk 8198

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-reg 8036 ax-inf2 8075

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 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 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 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-om 6700 df-recs 7060 df-rdg 7094 df-r1 8199 df-rank 8200

This theorem is referenced by: rankxpsuc 8317

W3C validator