pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8958

Description: A corollary of Konig's Theorem konigth 8944. 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 6665	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 194	. . 3 $\/$ $\/$ $/\$
3		cfom 8644	. . . . . . 7
4		aleph0 8447	. . . . . . . 8
5	4	fveq2i 5869	. . . . . . 7
6	3, 5, 4	3eqtr4i 2506	. . . . . 6
7		fveq2 5866	. . . . . . 7
8	7	fveq2d 5870	. . . . . 6
9	6, 8, 7	3eqtr4a 2534	. . . . 5
10		fvex 5876	. . . . . . . . 9
11	10	canth2 7670	. . . . . . . 8
12	10	pw2en 7624	. . . . . . . 8
13		sdomentr 7651	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 672	. . . . . . 7
15		alephon 8450	. . . . . . . . 9
16		alephgeom 8463	. . . . . . . . . 10
17		omelon 8063	. . . . . . . . . . . 12
18		2onn 7289	. . . . . . . . . . . 12
19		onelss 4920	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3512	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 670	. . . . . . . . . 10
23	16, 22	sylbi 195	. . . . . . . . 9
24		ssdomg 7561	. . . . . . . . 9
25	15, 23, 24	mpsyl 63	. . . . . . . 8
26		mapdom1 7682	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7650	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 663	. . . . . 6
30		oveq2 6292	. . . . . . 7
31	30	breq2d 4459	. . . . . 6
32	29, 31	syl5ibrcom 222	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 8957	. . . . . . 7
35		fveq2 5866	. . . . . . . 8
36	35	fveq2d 5870	. . . . . . 7
37	34, 36, 35	3eqtr4a 2534	. . . . . 6
38	37	rexlimivw 2952	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8651	. . . . . 6 $/\$ $/\$
41		limelon 4941	. . . . . . . . . . 11 $/\$
42		ffn 5731	. . . . . . . . . . . . . . . 16
43		fnrnfv 5914	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4255	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5876	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4359	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2526	. . . . . . . . . . . . . 14
49	48	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 6018	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 471	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3526	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3214	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2955	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2874	. . . . . . . . . . . . . . . 16
58	57	imp 429	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8464	. . . . . . . . . . . . . . . 16
61	60	biimpi 194	. . . . . . . . . . . . . . 15
62		frn 5737	. . . . . . . . . . . . . . . 16
63	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8641	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 477	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2510	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 6019	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4985	. . . . . . . . . . . . . . . . 17
70		harcard 8359	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8356	. . . . . . . . . . . . . . . . . . . 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 7550	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 7989	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4450	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3211	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 63	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 20	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7987	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5866	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5870	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5948	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4459	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 232	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2878	. . . . . . . . . . . . . 14
93		fvex 5876	. . . . . . . . . . . . . . 15
94		eqid 2467	. . . . . . . . . . . . . . 15
95		eqid 2467	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8944	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4469	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 471	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6309	. . . . . . . . . . . 12
102	68	ex 434	. . . . . . . . . . . . . . . 16
103		alephlim 8448	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2537	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4330	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8451	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8354	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7643	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8450	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4912	. . . . . . . . . . . . . . . . . . . . . . . . 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 8458	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4925	. . . . . . . . . . . . . . . . . . . . . . 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 2953	. . . . . . . . . . . . . . . . . . 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 4538	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2496	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 6045	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 6019	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4920	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 63	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2878	. . . . . . . . . . . . 13
139		ss2ixp 7482	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7479	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3550	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 20	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7561	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 63	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7650	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 435	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1015	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1698	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1292	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8446	. . . . 5
156		fndm 5680	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2545	. . 3
159		ndmfv 5890	. . . 4
160		1n0 7145	. . . . . 6
161		1on 7137	. . . . . . . 8
162	161	elexi 3123	. . . . . . 7
163	162	0sdom 7648	. . . . . 6
164	160, 163	mpbir 209	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5866	. . . . . . . . 9
167		cf0 8631	. . . . . . . . 9
168	166, 167	syl6eq 2524	. . . . . . . 8
169	165, 168	oveq12d 6302	. . . . . . 7
170		0ex 4577	. . . . . . . 8
171		map0e 7456	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2524	. . . . . 6
174	165, 173	breq12d 4460	. . . . 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 972 $/\$ w3a 973

wceq 1379

wex 1596

wcel 1767

cab 2452

wne 2662

wral 2814

wrex 2815

cvv 3113

wss 3476

c0 3785

cpw 4010

cuni 4245

ciun 4325 class class class wbr 4447

cmpt 4505

con0 4878

wlim 4879

csuc 4880

cdm 4999

crn 5000

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

com 6684

wsmo 7016

c1o 7123

c2o 7124

cmap 7420

cixp 7469

cen 7513

cdom 7514

csdm 7515 harchar 7982

ccrd 8316

cale 8317

ccf 8318

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-ac2 8843

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-smo 7017 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-oi 7935 df-har 7984 df-card 8320 df-aleph 8321 df-cf 8322 df-acn 8323 df-ac 8497

This theorem is referenced by: cfpwsdom 8959 tskcard 9159 bj-pwcfsdom 33688

W3C validator