pwcfsdom - Metamath Proof Explorer

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

Theorem pwcfsdom 8743

Description: A corollary of Konig's Theorem konigth 8729. 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 6456	. . . 4 $\/$ $\/$ $/\$
2	1	biimpi 194	. . 3 $\/$ $\/$ $/\$
3		cfom 8429	. . . . . . 7
4		aleph0 8232	. . . . . . . 8
5	4	fveq2i 5691	. . . . . . 7
6	3, 5, 4	3eqtr4i 2471	. . . . . 6
7		fveq2 5688	. . . . . . 7
8	7	fveq2d 5692	. . . . . 6
9	6, 8, 7	3eqtr4a 2499	. . . . 5
10		fvex 5698	. . . . . . . . 9
11	10	canth2 7460	. . . . . . . 8
12	10	pw2en 7414	. . . . . . . 8
13		sdomentr 7441	. . . . . . . 8 $/\$
14	11, 12, 13	mp2an 667	. . . . . . 7
15		alephon 8235	. . . . . . . . 9
16		alephgeom 8248	. . . . . . . . . 10
17		omelon 7848	. . . . . . . . . . . 12
18		2onn 7075	. . . . . . . . . . . 12
19		onelss 4757	. . . . . . . . . . . 12
20	17, 18, 19	mp2 9	. . . . . . . . . . 11
21		sstr 3361	. . . . . . . . . . 11 $/\$
22	20, 21	mpan 665	. . . . . . . . . 10
23	16, 22	sylbi 195	. . . . . . . . 9
24		ssdomg 7351	. . . . . . . . 9
25	15, 23, 24	mpsyl 63	. . . . . . . 8
26		mapdom1 7472	. . . . . . . 8
27	25, 26	syl 16	. . . . . . 7
28		sdomdomtr 7440	. . . . . . 7 $/\$
29	14, 27, 28	sylancr 658	. . . . . 6
30		oveq2 6098	. . . . . . 7
31	30	breq2d 4301	. . . . . 6
32	29, 31	syl5ibrcom 222	. . . . 5
33	9, 32	syl5 32	. . . 4
34		alephreg 8742	. . . . . . 7
35		fveq2 5688	. . . . . . . 8
36	35	fveq2d 5692	. . . . . . 7
37	34, 36, 35	3eqtr4a 2499	. . . . . 6
38	37	rexlimivw 2835	. . . . 5
39	38, 32	syl5 32	. . . 4
40		cfsmo 8436	. . . . . 6 $/\$ $/\$
41		limelon 4778	. . . . . . . . . . 11 $/\$
42		ffn 5556	. . . . . . . . . . . . . . . 16
43		fnrnfv 5735	. . . . . . . . . . . . . . . . 17
44	43	unieqd 4098	. . . . . . . . . . . . . . . 16
45	42, 44	syl 16	. . . . . . . . . . . . . . 15
46		fvex 5698	. . . . . . . . . . . . . . . 16
47	46	dfiun2 4201	. . . . . . . . . . . . . . 15
48	45, 47	syl6eqr 2491	. . . . . . . . . . . . . 14
49	48	ad2antrl 722	. . . . . . . . . . . . 13 $/\$ $/\$
50		fnfvelrn 5837	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	42, 50	sylan 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
52		sseq2 3375	. . . . . . . . . . . . . . . . . . . . 21
53	52	rspcev 3070	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	51, 53	sylan 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$
56	55	rexlimdva 2839	. . . . . . . . . . . . . . . . 17
57	56	ralimdv 2793	. . . . . . . . . . . . . . . 16
58	57	imp 429	. . . . . . . . . . . . . . 15 $/\$
59	58	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$
60		alephislim 8249	. . . . . . . . . . . . . . . 16
61	60	biimpi 194	. . . . . . . . . . . . . . 15
62		frn 5562	. . . . . . . . . . . . . . . 16
63	62	adantr 462	. . . . . . . . . . . . . . 15 $/\$
64		coflim 8426	. . . . . . . . . . . . . . 15 $/\$
65	61, 63, 64	syl2an 474	. . . . . . . . . . . . . 14 $/\$ $/\$
66	59, 65	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
67	49, 66	eqtr3d 2475	. . . . . . . . . . . 12 $/\$ $/\$
68		ffvelrn 5838	. . . . . . . . . . . . . . . . 17 $/\$
69	15	oneli 4822	. . . . . . . . . . . . . . . . 17
70		harcard 8144	. . . . . . . . . . . . . . . . . . 19 har har
71		iscard 8141	. . . . . . . . . . . . . . . . . . . 20 har har har $/\$ har har
72	71	simprbi 461	. . . . . . . . . . . . . . . . . . 19 har har har har
73	70, 72	ax-mp 5	. . . . . . . . . . . . . . . . . 18 har har
74		domrefg 7340	. . . . . . . . . . . . . . . . . . . 20
75	46, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
76		elharval 7774	. . . . . . . . . . . . . . . . . . . 20 har $/\$
77	76	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ har
78	75, 77	mpan2 666	. . . . . . . . . . . . . . . . . 18 har
79		breq1 4292	. . . . . . . . . . . . . . . . . . 19 har har
80	79	rspccv 3067	. . . . . . . . . . . . . . . . . 18 har har har har
81	73, 78, 80	mpsyl 63	. . . . . . . . . . . . . . . . 17 har
82	68, 69, 81	3syl 20	. . . . . . . . . . . . . . . 16 $/\$ har
83		harcl 7772	. . . . . . . . . . . . . . . . . . 19 har
84		fveq2 5688	. . . . . . . . . . . . . . . . . . . . 21
85	84	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20 har har
86		pwcfsdom.1	. . . . . . . . . . . . . . . . . . . 20 har
87	85, 86	fvmptg 5769	. . . . . . . . . . . . . . . . . . 19 $/\$ har har
88	83, 87	mpan2 666	. . . . . . . . . . . . . . . . . 18 har
89	88	breq2d 4301	. . . . . . . . . . . . . . . . 17 har
90	89	adantl 463	. . . . . . . . . . . . . . . 16 $/\$ har
91	82, 90	mpbird 232	. . . . . . . . . . . . . . 15 $/\$
92	91	ralrimiva 2797	. . . . . . . . . . . . . 14
93		fvex 5698	. . . . . . . . . . . . . . 15
94		eqid 2441	. . . . . . . . . . . . . . 15
95		eqid 2441	. . . . . . . . . . . . . . 15
96	93, 94, 95	konigth 8729	. . . . . . . . . . . . . 14
97	92, 96	syl 16	. . . . . . . . . . . . 13
98	97	ad2antrl 722	. . . . . . . . . . . 12 $/\$ $/\$
99	67, 98	eqbrtrrd 4311	. . . . . . . . . . 11 $/\$ $/\$
100	41, 99	sylan 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
101		ovex 6115	. . . . . . . . . . . 12
102	68	ex 434	. . . . . . . . . . . . . . . 16
103		alephlim 8233	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	eleq2d 2508	. . . . . . . . . . . . . . . . 17 $/\$
105		eliun 4172	. . . . . . . . . . . . . . . . . . 19
106		alephcard 8236	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	eleq2i 2505	. . . . . . . . . . . . . . . . . . . . . . . 24
108		cardsdomelir 8139	. . . . . . . . . . . . . . . . . . . . . . . 24
109	107, 108	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
110		elharval 7774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 har $/\$
111	110	simprbi 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 har
112		domnsym 7433	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 har
114	113	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . 24 har
115		alephon 8235	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		ontri1 4749	. . . . . . . . . . . . . . . . . . . . . . . . 25 har $/\$ har har
117	83, 115, 116	mp2an 667	. . . . . . . . . . . . . . . . . . . . . . . 24 har har
118	114, 117	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23 har
119	109, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 har
120		alephord2i 8243	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		ontr2 4762	. . . . . . . . . . . . . . . . . . . . . . 23 har $/\$ har $/\$ har
123	83, 15, 122	mp2an 667	. . . . . . . . . . . . . . . . . . . . . 22 har $/\$ har
124	119, 121, 123	syl2anr 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ har
125	124	exp31 601	. . . . . . . . . . . . . . . . . . . 20 har
126	125	rexlimdv 2838	. . . . . . . . . . . . . . . . . . 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 653	. . . . . . . . . . . . . . 15 $/\$ $/\$ har
131	130	imp 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ har
132	85	cbvmptv 4380	. . . . . . . . . . . . . . 15 har har
133	86, 132	eqtri 2461	. . . . . . . . . . . . . 14 har
134	131, 133	fmptd 5864	. . . . . . . . . . . . 13 $/\$ $/\$
135		ffvelrn 5838	. . . . . . . . . . . . . . 15 $/\$
136		onelss 4757	. . . . . . . . . . . . . . 15
137	15, 135, 136	mpsyl 63	. . . . . . . . . . . . . 14 $/\$
138	137	ralrimiva 2797	. . . . . . . . . . . . 13
139		ss2ixp 7272	. . . . . . . . . . . . . 14
140	93, 10	ixpconst 7269	. . . . . . . . . . . . . 14
141	139, 140	syl6sseq 3399	. . . . . . . . . . . . 13
142	134, 138, 141	3syl 20	. . . . . . . . . . . 12 $/\$ $/\$
143		ssdomg 7351	. . . . . . . . . . . 12
144	101, 142, 143	mpsyl 63	. . . . . . . . . . 11 $/\$ $/\$
145	144	adantrr 711	. . . . . . . . . 10 $/\$ $/\$ $/\$
146		sdomdomtr 7440	. . . . . . . . . 10 $/\$
147	100, 145, 146	syl2anc 656	. . . . . . . . 9 $/\$ $/\$ $/\$
148	147	expcom 435	. . . . . . . 8 $/\$ $/\$
149	148	3adant2 1002	. . . . . . 7 $/\$ $/\$ $/\$
150	149	exlimiv 1693	. . . . . 6 $/\$ $/\$ $/\$
151	15, 40, 150	mp2b 10	. . . . 5 $/\$
152	151	a1i 11	. . . 4 $/\$
153	33, 39, 152	3jaod 1277	. . 3 $\/$ $\/$ $/\$
154	2, 153	mpd 15	. 2
155		alephfnon 8231	. . . . 5
156		fndm 5507	. . . . 5
157	155, 156	ax-mp 5	. . . 4
158	157	eleq2i 2505	. . 3
159		ndmfv 5711	. . . 4
160		1n0 6931	. . . . . 6
161		1on 6923	. . . . . . . 8
162	161	elexi 2980	. . . . . . 7
163	162	0sdom 7438	. . . . . 6
164	160, 163	mpbir 209	. . . . 5
165		id 22	. . . . . 6
166		fveq2 5688	. . . . . . . . 9
167		cf0 8416	. . . . . . . . 9
168	166, 167	syl6eq 2489	. . . . . . . 8
169	165, 168	oveq12d 6108	. . . . . . 7
170		0ex 4419	. . . . . . . 8
171		map0e 7246	. . . . . . . 8
172	170, 171	ax-mp 5	. . . . . . 7
173	169, 172	syl6eq 2489	. . . . . 6
174	165, 173	breq12d 4302	. . . . 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 959 $/\$ w3a 960

wceq 1364

wex 1591

wcel 1761

cab 2427

wne 2604

wral 2713

wrex 2714

cvv 2970

wss 3325

c0 3634

cpw 3857

cuni 4088

ciun 4168 class class class wbr 4289

cmpt 4347

con0 4715

wlim 4716

csuc 4717

cdm 4836

crn 4837

wfn 5410

wf 5411

cfv 5415 (class class class)co 6090

com 6475

wsmo 6802

c1o 6909

c2o 6910

cmap 7210

cixp 7259

cen 7303

cdom 7304

csdm 7305 harchar 7767

ccrd 8101

cale 8102

ccf 8103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-ac2 8628

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-iin 4171 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-smo 6803 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-ixp 7260 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-oi 7720 df-har 7769 df-card 8105 df-aleph 8106 df-cf 8107 df-acn 8108 df-ac 8282

This theorem is referenced by: cfpwsdom 8744 tskcard 8944

W3C validator