pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8414

Description: A corollary of Konig's Theorem konigth 8400. 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 4785	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 187	. . 3 $\/$ $\/$ $/\$
3		cfom 8100	. . . . . . 7
4		aleph0 7903	. . . . . . . 8
5	4	fveq2i 5690	. . . . . . 7
6	3, 5, 4	3eqtr4i 2434	. . . . . 6
7		fveq2 5687	. . . . . . 7
8	7	fveq2d 5691	. . . . . 6
9	6, 8, 7	3eqtr4a 2462	. . . . 5
10		fvex 5701	. . . . . . . . 9
11	10	canth2 7219	. . . . . . . 8
12	10	pw2en 7174	. . . . . . . 8
13		sdomentr 7200	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 654	. . . . . . 7
15		alephon 7906	. . . . . . . . 9
16		alephgeom 7919	. . . . . . . . . 10
17		omelon 7557	. . . . . . . . . . . 12
18		2onn 6842	. . . . . . . . . . . 12
19		onelss 4583	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3316	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 652	. . . . . . . . . 10
23	16, 22	sylbi 188	. . . . . . . . 9
24		ssdomg 7112	. . . . . . . . 9
25	15, 23, 24	mpsyl 61	. . . . . . . 8
26		mapdom1 7231	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7199	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 645	. . . . . 6
30		oveq2 6048	. . . . . . 7
31	30	breq2d 4184	. . . . . 6
32	29, 31	syl5ibrcom 214	. . . . 5
33	9, 32	syl5 30	. . . 4
34		alephreg 8413	. . . . . . 7
35		fveq2 5687	. . . . . . . 8
36	35	fveq2d 5691	. . . . . . 7
37	34, 36, 35	3eqtr4a 2462	. . . . . 6
38	37	rexlimivw 2786	. . . . 5
39	38, 32	syl5 30	. . . 4
40		cfsmo 8107	. . . . . 6 $/\$ $/\$
41		limelon 4604	. . . . . . . . . . 11 $/\$
42		ffn 5550	. . . . . . . . . . . . . . . 16
43		fnrnfv 5732	. . . . . . . . . . . . . . . . 17
44	43	unieqd 3986	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5701	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4085	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2454	. . . . . . . . . . . . . 14
49	48	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 458	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3330	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3012	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 458	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 424	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2790	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2745	. . . . . . . . . . . . . . . 16
58	57	imp 419	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 7920	. . . . . . . . . . . . . . . 16
61	60	biimpi 187	. . . . . . . . . . . . . . 15
62		frn 5556	. . . . . . . . . . . . . . . 16
63	62	adantr 452	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8097	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 464	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 224	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2438	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 5827	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4648	. . . . . . . . . . . . . . . . 17
70		harcard 7821	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 7818	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 451	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 8	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7101	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 8	. . . . . . . . . . . . . . . . . . 19
76		elharval 7487	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 198	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 653	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4175	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3009	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 61	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 19	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7485	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5687	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5763	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 653	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4184	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 453	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 224	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2749	. . . . . . . . . . . . . 14
93		fvex 5701	. . . . . . . . . . . . . . 15
94		eqid 2404	. . . . . . . . . . . . . . 15
95		eqid 2404	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8400	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 709	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4194	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 458	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6065	. . . . . . . . . . . 12
102	68	ex 424	. . . . . . . . . . . . . . . 16
103		alephlim 7904	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2471	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4057	. . . . . . . . . . . . . . . . . . 19
106		alephcard 7907	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2468	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 7816	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 205	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7192	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 114	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 7906	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4575	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 654	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 7914	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 419	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4588	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 654	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 588	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2789	. . . . . . . . . . . . . . . . . . 19 har
127	105, 126	syl5bi 209	. . . . . . . . . . . . . . . . . 18 har
128	41, 127	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ har
129	104, 128	sylbid 207	. . . . . . . . . . . . . . . 16 $/\$ har
130	102, 129	sylan9r 640	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 419	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4260	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2424	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 5852	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 5827	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4583	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 61	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2749	. . . . . . . . . . . . 13
139		ss2ixp 7034	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7031	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3354	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 19	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7112	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 61	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 698	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7199	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 425	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 976	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1641	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1248	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 7902	. . . . 5
156		fndm 5503	. . . . 5
157	155, 156	ax-mp 8	. . . 4
158	157	eleq2i 2468	. . 3
159		ndmfv 5714	. . . 4
160		1n0 6698	. . . . . 6
161		1on 6690	. . . . . . . 8
162	161	elexi 2925	. . . . . . 7
163	162	0sdom 7197	. . . . . 6
164	160, 163	mpbir 201	. . . . 5
165		id 20	. . . . . 6
166		fveq2 5687	. . . . . . . . 9
167		cf0 8087	. . . . . . . . 9
168	166, 167	syl6eq 2452	. . . . . . . 8
169	165, 168	oveq12d 6058	. . . . . . 7
170		0ex 4299	. . . . . . . 8
171		map0e 7010	. . . . . . . 8
172	170, 171	ax-mp 8	. . . . . . 7
173	169, 172	syl6eq 2452	. . . . . 6
174	165, 173	breq12d 4185	. . . . 5
175	164, 174	mpbiri 225	. . . 4
176	159, 175	syl 16	. . 3
177	158, 176	sylnbir 299	. 2
178	154, 177	pm2.61i 158	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $\/$ w3o 935 $/\$ w3a 936

wex 1547

wceq 1649

wcel 1721

cab 2390

wne 2567

wral 2666

wrex 2667

cvv 2916

wss 3280

c0 3588

cpw 3759

cuni 3975

ciun 4053 class class class wbr 4172

cmpt 4226

con0 4541

wlim 4542

csuc 4543

com 4804

cdm 4837

crn 4838

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

wsmo 6566

c1o 6676

c2o 6677

cmap 6977

cixp 7022

cen 7065

cdom 7066

csdm 7067 harchar 7480

ccrd 7778

cale 7779

ccf 7780

This theorem is referenced by: cfpwsdom 8415 tskcard 8612

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-ac2 8299

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-smo 6567 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-oi 7435 df-har 7482 df-card 7782 df-aleph 7783 df-cf 7784 df-acn 7785 df-ac 7953

W3C validator