pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8949

Description: A corollary of Konig's Theorem konigth 8935. 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 6654	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 194	. . 3 $\/$ $\/$ $/\$
3		cfom 8635	. . . . . . 7
4		aleph0 8438	. . . . . . . 8
5	4	fveq2i 5851	. . . . . . 7
6	3, 5, 4	3eqtr4i 2493	. . . . . 6
7		fveq2 5848	. . . . . . 7
8	7	fveq2d 5852	. . . . . 6
9	6, 8, 7	3eqtr4a 2521	. . . . 5
10		fvex 5858	. . . . . . . . 9
11	10	canth2 7663	. . . . . . . 8
12	10	pw2en 7617	. . . . . . . 8
13		sdomentr 7644	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 670	. . . . . . 7
15		alephon 8441	. . . . . . . . 9
16		alephgeom 8454	. . . . . . . . . 10
17		omelon 8054	. . . . . . . . . . . 12
18		2onn 7281	. . . . . . . . . . . 12
19		onelss 4909	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3497	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 668	. . . . . . . . . 10
23	16, 22	sylbi 195	. . . . . . . . 9
24		ssdomg 7554	. . . . . . . . 9
25	15, 23, 24	mpsyl 63	. . . . . . . 8
26		mapdom1 7675	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7643	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 661	. . . . . 6
30		oveq2 6278	. . . . . . 7
31	30	breq2d 4451	. . . . . 6
32	29, 31	syl5ibrcom 222	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 8948	. . . . . . 7
35		fveq2 5848	. . . . . . . 8
36	35	fveq2d 5852	. . . . . . 7
37	34, 36, 35	3eqtr4a 2521	. . . . . 6
38	37	rexlimivw 2943	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8642	. . . . . 6 $/\$ $/\$
41		limelon 4930	. . . . . . . . . . 11 $/\$
42		ffn 5713	. . . . . . . . . . . . . . . 16
43		fnrnfv 5894	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4245	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5858	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4349	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2513	. . . . . . . . . . . . . 14
49	48	ad2antrl 725	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 6004	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 469	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3511	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3207	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 469	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 432	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2946	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2864	. . . . . . . . . . . . . . . 16
58	57	imp 427	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8455	. . . . . . . . . . . . . . . 16
61	60	biimpi 194	. . . . . . . . . . . . . . 15
62		frn 5719	. . . . . . . . . . . . . . . 16
63	62	adantr 463	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8632	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 475	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2497	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 6005	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4974	. . . . . . . . . . . . . . . . 17
70		harcard 8350	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8347	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 462	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 5	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7543	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 7981	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 669	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4442	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3204	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 63	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 20	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7979	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5929	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 669	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4451	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 464	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 232	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2868	. . . . . . . . . . . . . 14
93		fvex 5858	. . . . . . . . . . . . . . 15
94		eqid 2454	. . . . . . . . . . . . . . 15
95		eqid 2454	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8935	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 725	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4461	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 469	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6298	. . . . . . . . . . . 12
102	68	ex 432	. . . . . . . . . . . . . . . 16
103		alephlim 8439	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2524	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4320	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8442	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2532	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8345	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7981	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7636	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8441	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4901	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 8449	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 427	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4914	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 670	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 476	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 602	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2944	. . . . . . . . . . . . . . . . . . 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 656	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 427	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4530	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2483	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 6031	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 6005	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4909	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 63	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2868	. . . . . . . . . . . . 13
139		ss2ixp 7475	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7472	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3535	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 20	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7554	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 63	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 714	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7643	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 433	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1013	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1727	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1290	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8437	. . . . 5
156		fndm 5662	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2532	. . 3
159		ndmfv 5872	. . . 4
160		1n0 7137	. . . . . 6
161		1on 7129	. . . . . . . 8
162	161	elexi 3116	. . . . . . 7
163	162	0sdom 7641	. . . . . 6
164	160, 163	mpbir 209	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5848	. . . . . . . . 9
167		cf0 8622	. . . . . . . . 9
168	166, 167	syl6eq 2511	. . . . . . . 8
169	165, 168	oveq12d 6288	. . . . . . 7
170		0ex 4569	. . . . . . . 8
171		map0e 7449	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2511	. . . . . 6
174	165, 173	breq12d 4452	. . . . 5
175	164, 174	mpbiri 233	. . . 4
176	159, 175	syl 16	. . 3
177	158, 176	sylnbir 305	. 2
178	154, 177	pm2.61i 164	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $\/$ w3o 970 $/\$ w3a 971

wceq 1398

wex 1617

wcel 1823

cab 2439

wne 2649

wral 2804

wrex 2805

cvv 3106

wss 3461

c0 3783

cpw 3999

cuni 4235

ciun 4315 class class class wbr 4439

cmpt 4497

con0 4867

wlim 4868

csuc 4869

cdm 4988

crn 4989

wfn 5565

wf 5566

cfv 5570 (class class class)co 6270

com 6673

wsmo 7008

c1o 7115

c2o 7116

cmap 7412

cixp 7462

cen 7506

cdom 7507

csdm 7508 harchar 7974

ccrd 8307

cale 8308

ccf 8309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049 ax-ac2 8834

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-iin 4318 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-smo 7009 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-er 7303 df-map 7414 df-ixp 7463 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-oi 7927 df-har 7976 df-card 8311 df-aleph 8312 df-cf 8313 df-acn 8314 df-ac 8488

This theorem is referenced by: cfpwsdom 8950 tskcard 9148 bj-pwcfsdom 35009

W3C validator