pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 9006

Description: A corollary of Konig's Theorem konigth 8992. 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 6687	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 197	. . 3 $\/$ $\/$ $/\$
3		cfom 8692	. . . . . . 7
4		aleph0 8495	. . . . . . . 8
5	4	fveq2i 5884	. . . . . . 7
6	3, 5, 4	3eqtr4i 2468	. . . . . 6
7		fveq2 5881	. . . . . . 7
8	7	fveq2d 5885	. . . . . 6
9	6, 8, 7	3eqtr4a 2496	. . . . 5
10		fvex 5891	. . . . . . . . 9
11	10	canth2 7731	. . . . . . . 8
12	10	pw2en 7685	. . . . . . . 8
13		sdomentr 7712	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 676	. . . . . . 7
15		alephon 8498	. . . . . . . . 9
16		alephgeom 8511	. . . . . . . . . 10
17		omelon 8151	. . . . . . . . . . . 12
18		2onn 7349	. . . . . . . . . . . 12
19		onelss 5484	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3478	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 674	. . . . . . . . . 10
23	16, 22	sylbi 198	. . . . . . . . 9
24		ssdomg 7622	. . . . . . . . 9
25	15, 23, 24	mpsyl 65	. . . . . . . 8
26		mapdom1 7743	. . . . . . . 8
27	25, 26	syl 17	. . . . . . 7
28		sdomdomtr 7711	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 667	. . . . . 6
30		oveq2 6313	. . . . . . 7
31	30	breq2d 4438	. . . . . 6
32	29, 31	syl5ibrcom 225	. . . . 5
33	9, 32	syl5 33	. . . 4
34		alephreg 9005	. . . . . . 7
35		fveq2 5881	. . . . . . . 8
36	35	fveq2d 5885	. . . . . . 7
37	34, 36, 35	3eqtr4a 2496	. . . . . 6
38	37	rexlimivw 2921	. . . . 5
39	38, 32	syl5 33	. . . 4
40		cfsmo 8699	. . . . . 6 $/\$ $/\$
41		limelon 5505	. . . . . . . . . . 11 $/\$
42		ffn 5746	. . . . . . . . . . . . . . . 16
43		fnrnfv 5927	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4232	. . . . . . . . . . . . . . . 16
45	42, 44	syl 17	. . . . . . . . . . . . . . 15
46		fvex 5891	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4336	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2488	. . . . . . . . . . . . . 14
49	48	ad2antrl 732	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3492	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3188	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 435	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2924	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2842	. . . . . . . . . . . . . . . 16
58	57	imp 430	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 467	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8512	. . . . . . . . . . . . . . . 16
61	60	biimpi 197	. . . . . . . . . . . . . . 15
62		frn 5752	. . . . . . . . . . . . . . . 16
63	62	adantr 466	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8689	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 479	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 235	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2472	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 6035	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 5549	. . . . . . . . . . . . . . . . 17
70		harcard 8411	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8408	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 465	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 5	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7611	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 8078	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 209	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 675	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4429	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3185	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 65	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 18	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 8076	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5885	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5962	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 675	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4438	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 467	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 235	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2846	. . . . . . . . . . . . . 14
93		fvex 5891	. . . . . . . . . . . . . . 15
94		eqid 2429	. . . . . . . . . . . . . . 15
95		eqid 2429	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8992	. . . . . . . . . . . . . 14
97	92, 96	syl 17	. . . . . . . . . . . . 13
98	97	ad2antrl 732	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4448	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 473	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6333	. . . . . . . . . . . 12
102	68	ex 435	. . . . . . . . . . . . . . . 16
103		alephlim 8496	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2499	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4307	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8499	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2507	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8406	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 216	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 8078	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7704	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 123	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8498	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 5476	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 8506	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 5489	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 676	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 607	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2922	. . . . . . . . . . . . . . . . . . 19 har
127	105, 126	syl5bi 220	. . . . . . . . . . . . . . . . . 18 har
128	41, 127	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ har
129	104, 128	sylbid 218	. . . . . . . . . . . . . . . 16 $/\$ har
130	102, 129	sylan9r 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 430	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4518	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2458	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 6061	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 6035	. . . . . . . . . . . . . . 15 $/\$
136		onelss 5484	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 65	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2846	. . . . . . . . . . . . 13
139		ss2ixp 7543	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7540	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3516	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 18	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7622	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 65	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 721	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7711	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 436	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1024	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1769	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1328	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8494	. . . . 5
156		fndm 5693	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2507	. . 3
159		ndmfv 5905	. . . 4
160		1n0 7205	. . . . . 6
161		1on 7197	. . . . . . . 8
162	161	elexi 3097	. . . . . . 7
163	162	0sdom 7709	. . . . . 6
164	160, 163	mpbir 212	. . . . 5
165		id 23	. . . . . 6
166		fveq2 5881	. . . . . . . . 9
167		cf0 8679	. . . . . . . . 9
168	166, 167	syl6eq 2486	. . . . . . . 8
169	165, 168	oveq12d 6323	. . . . . . 7
170		0ex 4557	. . . . . . . 8
171		map0e 7517	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2486	. . . . . 6
174	165, 173	breq12d 4439	. . . . 5
175	164, 174	mpbiri 236	. . . 4
176	159, 175	syl 17	. . 3
177	158, 176	sylnbir 308	. 2
178	154, 177	pm2.61i 167	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $\/$ w3o 981 $/\$ w3a 982

wceq 1437

wex 1659

wcel 1870

cab 2414

wne 2625

wral 2782

wrex 2783

cvv 3087

wss 3442

c0 3767

cpw 3985

cuni 4222

ciun 4302 class class class wbr 4426

cmpt 4484

cdm 4854

crn 4855

con0 5442

wlim 5443

csuc 5444

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

com 6706

wsmo 7072

c1o 7183

c2o 7184

cmap 7480

cixp 7530

cen 7574

cdom 7575

csdm 7576 harchar 8071

ccrd 8368

cale 8369

ccf 8370

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-ac2 8891

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-iin 4305 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-smo 7073 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-ixp 7531 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-oi 8025 df-har 8073 df-card 8372 df-aleph 8373 df-cf 8374 df-acn 8375 df-ac 8545

This theorem is referenced by: cfpwsdom 9007 tskcard 9205 bj-pwcfsdom 31374

W3C validator