pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 9026

Description: A corollary of Konig's Theorem konigth 9012. 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 6692	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 199	. . 3 $\/$ $\/$ $/\$
3		cfom 8712	. . . . . . 7
4		aleph0 8515	. . . . . . . 8
5	4	fveq2i 5882	. . . . . . 7
6	3, 5, 4	3eqtr4i 2503	. . . . . 6
7		fveq2 5879	. . . . . . 7
8	7	fveq2d 5883	. . . . . 6
9	6, 8, 7	3eqtr4a 2531	. . . . 5
10		fvex 5889	. . . . . . . . 9
11	10	canth2 7743	. . . . . . . 8
12	10	pw2en 7697	. . . . . . . 8
13		sdomentr 7724	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 686	. . . . . . 7
15		alephon 8518	. . . . . . . . 9
16		alephgeom 8531	. . . . . . . . . 10
17		omelon 8169	. . . . . . . . . . . 12
18		2onn 7359	. . . . . . . . . . . 12
19		onelss 5472	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3426	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 684	. . . . . . . . . 10
23	16, 22	sylbi 200	. . . . . . . . 9
24		ssdomg 7633	. . . . . . . . 9
25	15, 23, 24	mpsyl 64	. . . . . . . 8
26		mapdom1 7755	. . . . . . . 8
27	25, 26	syl 17	. . . . . . 7
28		sdomdomtr 7723	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 676	. . . . . 6
30		oveq2 6316	. . . . . . 7
31	30	breq2d 4407	. . . . . 6
32	29, 31	syl5ibrcom 230	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 9025	. . . . . . 7
35		fveq2 5879	. . . . . . . 8
36	35	fveq2d 5883	. . . . . . 7
37	34, 36, 35	3eqtr4a 2531	. . . . . 6
38	37	rexlimivw 2869	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8719	. . . . . 6 $/\$ $/\$
41		limelon 5493	. . . . . . . . . . 11 $/\$
42		ffn 5739	. . . . . . . . . . . . . . . 16
43		fnrnfv 5925	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4200	. . . . . . . . . . . . . . . 16
45	42, 44	syl 17	. . . . . . . . . . . . . . 15
46		fvex 5889	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4303	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2523	. . . . . . . . . . . . . 14
49	48	ad2antrl 742	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 479	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3440	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3136	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 479	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 441	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2871	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2806	. . . . . . . . . . . . . . . 16
58	57	imp 436	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8532	. . . . . . . . . . . . . . . 16
61	60	biimpi 199	. . . . . . . . . . . . . . 15
62		frn 5747	. . . . . . . . . . . . . . . 16
63	62	adantr 472	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8709	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 485	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 240	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2507	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 6035	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 5537	. . . . . . . . . . . . . . . . 17
70		harcard 8430	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8427	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 471	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 5	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7622	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 8096	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 211	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 685	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4398	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3133	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 64	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 18	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 8094	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5961	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 685	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4407	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 240	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2809	. . . . . . . . . . . . . 14
93		fvex 5889	. . . . . . . . . . . . . . 15
94		eqid 2471	. . . . . . . . . . . . . . 15
95		eqid 2471	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 9012	. . . . . . . . . . . . . 14
97	92, 96	syl 17	. . . . . . . . . . . . 13
98	97	ad2antrl 742	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4418	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 479	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6336	. . . . . . . . . . . 12
102	68	ex 441	. . . . . . . . . . . . . . . 16
103		alephlim 8516	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2534	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4274	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8519	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8425	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 8096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7716	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 124	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8518	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 5464	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 686	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 8526	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 436	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 5477	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 686	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 615	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2870	. . . . . . . . . . . . . . . . . . 19 har
127	105, 126	syl5bi 225	. . . . . . . . . . . . . . . . . 18 har
128	41, 127	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ har
129	104, 128	sylbid 223	. . . . . . . . . . . . . . . 16 $/\$ har
130	102, 129	sylan9r 670	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4488	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2493	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 6061	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 6035	. . . . . . . . . . . . . . 15 $/\$
136		onelss 5472	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 64	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2809	. . . . . . . . . . . . 13
139		ss2ixp 7553	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7550	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3464	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 18	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7633	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 64	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7723	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 442	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1049	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1784	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1358	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8514	. . . . 5
156		fndm 5685	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2541	. . 3
159		ndmfv 5903	. . . 4
160		1n0 7215	. . . . . 6
161		1on 7207	. . . . . . . 8
162	161	elexi 3041	. . . . . . 7
163	162	0sdom 7721	. . . . . 6
164	160, 163	mpbir 214	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5879	. . . . . . . . 9
167		cf0 8699	. . . . . . . . 9
168	166, 167	syl6eq 2521	. . . . . . . 8
169	165, 168	oveq12d 6326	. . . . . . 7
170		0ex 4528	. . . . . . . 8
171		map0e 7527	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2521	. . . . . 6
174	165, 173	breq12d 4408	. . . . 5
175	164, 174	mpbiri 241	. . . 4
176	159, 175	syl 17	. . 3
177	158, 176	sylnbir 314	. 2
178	154, 177	pm2.61i 169	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

cab 2457

wne 2641

wral 2756

wrex 2757

cvv 3031

wss 3390

c0 3722

cpw 3942

cuni 4190

ciun 4269 class class class wbr 4395

cmpt 4454

cdm 4839

crn 4840

con0 5430

wlim 5431

csuc 5432

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

com 6711

wsmo 7082

c1o 7193

c2o 7194

cmap 7490

cixp 7540

cen 7584

cdom 7585

csdm 7586 harchar 8089

ccrd 8387

cale 8388

ccf 8389

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-ac2 8911

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-smo 7083 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-oi 8043 df-har 8091 df-card 8391 df-aleph 8392 df-cf 8393 df-acn 8394 df-ac 8565

This theorem is referenced by: cfpwsdom 9027 tskcard 9224 bj-pwcfsdom 31696

W3C validator