pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8747

Description: A corollary of Konig's Theorem konigth 8733. 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 6457	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 194	. . 3 $\/$ $\/$ $/\$
3		cfom 8433	. . . . . . 7
4		aleph0 8236	. . . . . . . 8
5	4	fveq2i 5694	. . . . . . 7
6	3, 5, 4	3eqtr4i 2473	. . . . . 6
7		fveq2 5691	. . . . . . 7
8	7	fveq2d 5695	. . . . . 6
9	6, 8, 7	3eqtr4a 2501	. . . . 5
10		fvex 5701	. . . . . . . . 9
11	10	canth2 7464	. . . . . . . 8
12	10	pw2en 7418	. . . . . . . 8
13		sdomentr 7445	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 672	. . . . . . 7
15		alephon 8239	. . . . . . . . 9
16		alephgeom 8252	. . . . . . . . . 10
17		omelon 7852	. . . . . . . . . . . 12
18		2onn 7079	. . . . . . . . . . . 12
19		onelss 4761	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3364	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 670	. . . . . . . . . 10
23	16, 22	sylbi 195	. . . . . . . . 9
24		ssdomg 7355	. . . . . . . . 9
25	15, 23, 24	mpsyl 63	. . . . . . . 8
26		mapdom1 7476	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7444	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 663	. . . . . 6
30		oveq2 6099	. . . . . . 7
31	30	breq2d 4304	. . . . . 6
32	29, 31	syl5ibrcom 222	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 8746	. . . . . . 7
35		fveq2 5691	. . . . . . . 8
36	35	fveq2d 5695	. . . . . . 7
37	34, 36, 35	3eqtr4a 2501	. . . . . 6
38	37	rexlimivw 2837	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8440	. . . . . 6 $/\$ $/\$
41		limelon 4782	. . . . . . . . . . 11 $/\$
42		ffn 5559	. . . . . . . . . . . . . . . 16
43		fnrnfv 5738	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4101	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5701	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4204	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2493	. . . . . . . . . . . . . 14
49	48	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 5840	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 471	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3378	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3073	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2841	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2795	. . . . . . . . . . . . . . . 16
58	57	imp 429	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8253	. . . . . . . . . . . . . . . 16
61	60	biimpi 194	. . . . . . . . . . . . . . 15
62		frn 5565	. . . . . . . . . . . . . . . 16
63	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8430	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 477	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2477	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 5841	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4826	. . . . . . . . . . . . . . . . 17
70		harcard 8148	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8145	. . . . . . . . . . . . . . . . . . . 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 7344	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 7778	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4295	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3070	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 63	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 20	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7776	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5691	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5695	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5772	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 671	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4304	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 232	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2799	. . . . . . . . . . . . . 14
93		fvex 5701	. . . . . . . . . . . . . . 15
94		eqid 2443	. . . . . . . . . . . . . . 15
95		eqid 2443	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8733	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4314	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 471	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6116	. . . . . . . . . . . 12
102	68	ex 434	. . . . . . . . . . . . . . . 16
103		alephlim 8237	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2510	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4175	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8240	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2507	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8143	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7437	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8239	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4753	. . . . . . . . . . . . . . . . . . . . . . . . 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 8247	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4766	. . . . . . . . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . . . . . 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 4383	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2463	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 5867	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 5841	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4761	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 63	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2799	. . . . . . . . . . . . 13
139		ss2ixp 7276	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7273	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3402	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 20	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7355	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 63	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7444	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 435	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1007	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1688	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1282	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8235	. . . . 5
156		fndm 5510	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2507	. . 3
159		ndmfv 5714	. . . 4
160		1n0 6935	. . . . . 6
161		1on 6927	. . . . . . . 8
162	161	elexi 2982	. . . . . . 7
163	162	0sdom 7442	. . . . . 6
164	160, 163	mpbir 209	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5691	. . . . . . . . 9
167		cf0 8420	. . . . . . . . 9
168	166, 167	syl6eq 2491	. . . . . . . 8
169	165, 168	oveq12d 6109	. . . . . . 7
170		0ex 4422	. . . . . . . 8
171		map0e 7250	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2491	. . . . . 6
174	165, 173	breq12d 4305	. . . . 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 964 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

cab 2429

wne 2606

wral 2715

wrex 2716

cvv 2972

wss 3328

c0 3637

cpw 3860

cuni 4091

ciun 4171 class class class wbr 4292

cmpt 4350

con0 4719

wlim 4720

csuc 4721

cdm 4840

crn 4841

wfn 5413

wf 5414

cfv 5418 (class class class)co 6091

com 6476

wsmo 6806

c1o 6913

c2o 6914

cmap 7214

cixp 7263

cen 7307

cdom 7308

csdm 7309 harchar 7771

ccrd 8105

cale 8106

ccf 8107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-inf2 7847 ax-ac2 8632

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-iin 4174 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-se 4680 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-isom 5427 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-smo 6807 df-recs 6832 df-rdg 6866 df-1o 6920 df-2o 6921 df-oadd 6924 df-er 7101 df-map 7216 df-ixp 7264 df-en 7311 df-dom 7312 df-sdom 7313 df-fin 7314 df-oi 7724 df-har 7773 df-card 8109 df-aleph 8110 df-cf 8111 df-acn 8112 df-ac 8286

This theorem is referenced by: cfpwsdom 8748 tskcard 8948 bj-pwcfsdom 32519

W3C validator