pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8956

Description: A corollary of Konig's Theorem konigth 8942. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)

**Hypothesis**
Ref	Expression
pwcfsdom.1	har

**Assertion**
Ref	Expression
pwcfsdom

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem pwcfsdom Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onzsl 6662	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 194	. . 3 $\/$ $\/$ $/\$
3		cfom 8642	. . . . . . 7
4		aleph0 8445	. . . . . . . 8
5	4	fveq2i 5855	. . . . . . 7
6	3, 5, 4	3eqtr4i 2480	. . . . . 6
7		fveq2 5852	. . . . . . 7
8	7	fveq2d 5856	. . . . . 6
9	6, 8, 7	3eqtr4a 2508	. . . . 5
10		fvex 5862	. . . . . . . . 9
11	10	canth2 7668	. . . . . . . 8
12	10	pw2en 7622	. . . . . . . 8
13		sdomentr 7649	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 672	. . . . . . 7
15		alephon 8448	. . . . . . . . 9
16		alephgeom 8461	. . . . . . . . . 10
17		omelon 8061	. . . . . . . . . . . 12
18		2onn 7287	. . . . . . . . . . . 12
19		onelss 4906	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3494	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 670	. . . . . . . . . 10
23	16, 22	sylbi 195	. . . . . . . . 9
24		ssdomg 7559	. . . . . . . . 9
25	15, 23, 24	mpsyl 63	. . . . . . . 8
26		mapdom1 7680	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7648	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 663	. . . . . 6
30		oveq2 6285	. . . . . . 7
31	30	breq2d 4445	. . . . . 6
32	29, 31	syl5ibrcom 222	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 8955	. . . . . . 7
35		fveq2 5852	. . . . . . . 8
36	35	fveq2d 5856	. . . . . . 7
37	34, 36, 35	3eqtr4a 2508	. . . . . 6
38	37	rexlimivw 2930	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8649	. . . . . 6 $/\$ $/\$
41		limelon 4927	. . . . . . . . . . 11 $/\$
42		ffn 5717	. . . . . . . . . . . . . . . 16
43		fnrnfv 5900	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4240	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5862	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4345	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2500	. . . . . . . . . . . . . 14
49	48	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 6009	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 471	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3508	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3194	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2933	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2851	. . . . . . . . . . . . . . . 16
58	57	imp 429	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8462	. . . . . . . . . . . . . . . 16
61	60	biimpi 194	. . . . . . . . . . . . . . 15
62		frn 5723	. . . . . . . . . . . . . . . 16
63	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8639	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 477	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2484	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 6010	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4971	. . . . . . . . . . . . . . . . 17
70		harcard 8357	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8354	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 464	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 5	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7548	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 7987	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4436	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3191	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 63	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 20	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7985	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5852	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5856	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5935	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4445	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 232	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2855	. . . . . . . . . . . . . 14
93		fvex 5862	. . . . . . . . . . . . . . 15
94		eqid 2441	. . . . . . . . . . . . . . 15
95		eqid 2441	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8942	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4455	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 471	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6305	. . . . . . . . . . . 12
102	68	ex 434	. . . . . . . . . . . . . . . 16
103		alephlim 8446	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2511	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4316	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8449	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2519	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8352	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7987	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7641	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8448	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4898	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 8456	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4911	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 672	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 604	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2931	. . . . . . . . . . . . . . . . . . 19 har
127	105, 126	syl5bi 217	. . . . . . . . . . . . . . . . . 18 har
128	41, 127	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ har
129	104, 128	sylbid 215	. . . . . . . . . . . . . . . 16 $/\$ har
130	102, 129	sylan9r 658	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4524	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2470	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 6036	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 6010	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4906	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 63	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2855	. . . . . . . . . . . . 13
139		ss2ixp 7480	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7477	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3532	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 20	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7559	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 63	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7648	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 435	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1014	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1707	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1291	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8444	. . . . 5
156		fndm 5666	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2519	. . 3
159		ndmfv 5876	. . . 4
160		1n0 7143	. . . . . 6
161		1on 7135	. . . . . . . 8
162	161	elexi 3103	. . . . . . 7
163	162	0sdom 7646	. . . . . 6
164	160, 163	mpbir 209	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5852	. . . . . . . . 9
167		cf0 8629	. . . . . . . . 9
168	166, 167	syl6eq 2498	. . . . . . . 8
169	165, 168	oveq12d 6295	. . . . . . 7
170		0ex 4563	. . . . . . . 8
171		map0e 7454	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2498	. . . . . 6
174	165, 173	breq12d 4446	. . . . 5
175	164, 174	mpbiri 233	. . . 4
176	159, 175	syl 16	. . 3
177	158, 176	sylnbir 307	. 2
178	154, 177	pm2.61i 164	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 971 $/\$ w3a 972

wceq 1381

wex 1597

wcel 1802

cab 2426

wne 2636

wral 2791

wrex 2792

cvv 3093

wss 3458

c0 3767

cpw 3993

cuni 4230

ciun 4311 class class class wbr 4433

cmpt 4491

con0 4864

wlim 4865

csuc 4866

cdm 4985

crn 4986

wfn 5569

wf 5570

cfv 5574 (class class class)co 6277

com 6681

wsmo 7014

c1o 7121

c2o 7122

cmap 7418

cixp 7467

cen 7511

cdom 7512

csdm 7513 harchar 7980

ccrd 8314

cale 8315

ccf 8316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-inf2 8056 ax-ac2 8841

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-int 4268 df-iun 4313 df-iin 4314 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-se 4825 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-isom 5583 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6682 df-1st 6781 df-2nd 6782 df-smo 7015 df-recs 7040 df-rdg 7074 df-1o 7128 df-2o 7129 df-oadd 7132 df-er 7309 df-map 7420 df-ixp 7468 df-en 7515 df-dom 7516 df-sdom 7517 df-fin 7518 df-oi 7933 df-har 7982 df-card 8318 df-aleph 8319 df-cf 8320 df-acn 8321 df-ac 8495

This theorem is referenced by: cfpwsdom 8957 tskcard 9157 bj-pwcfsdom 34301

W3C validator