fiint - Metamath Proof Explorer

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

Theorem fiint 7580

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of

is in

." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.)

**Assertion**
Ref	Expression
fiint	$/\$ $/\$

Distinct variable group:

Proof of Theorem fiint Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 7325	. . . . . . 7
2		ensym 7350	. . . . . . . . 9
3		breq1 4290	. . . . . . . . . . . . . . . 16
4	3	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1679	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4290	. . . . . . . . . . . . . . . 16
8	7	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1679	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4290	. . . . . . . . . . . . . . . 16
12	11	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1679	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7350	. . . . . . . . . . . . . . . . . . . 20
16		en0 7364	. . . . . . . . . . . . . . . . . . . 20
17	15, 16	sylib 196	. . . . . . . . . . . . . . . . . . 19
18	17	anim1i 568	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	18	ancoms 453	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	adantll 713	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		df-ne 2603	. . . . . . . . . . . . . . . . 17
22		pm3.24 877	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 131	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 475	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1591	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1673	. . . . . . . . . . . . . . 15
29		nfa1 1830	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7311	. . . . . . . . . . . . . . . . . . 19
31		f1of 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 5836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3345	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2603	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
74	73	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	68, 74	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
76	75	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
77	76	exp5c 616	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	77	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
79	78	imp43 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
80	40, 79	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
81		inteq 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5696	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4162	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4128	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2484	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 612	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1690	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	30, 114	syl5bi 217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	imp 429	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	116	adantlr 714	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
118	117	com13 80	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
119	28, 29, 118	alrimd 1815	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6499	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1794	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
123	121, 122	syl6 33	. . . . . . . . . . 11 $/\$ $/\$
124	123	exp4a 606	. . . . . . . . . 10 $/\$
125	124	com24 87	. . . . . . . . 9 $/\$
126	2, 125	syl5 32	. . . . . . . 8 $/\$
127	126	rexlimiv 2830	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	impd 431	. . . 4 $/\$ $/\$
131	130	alrimiv 1685	. . 3 $/\$ $/\$
132		zfpair2 4527	. . . . . 6
133		sseq1 3372	. . . . . . . . 9
134		neeq1 2611	. . . . . . . . 9
135	133, 134	anbi12d 710	. . . . . . . 8 $/\$ $/\$
136		eleq1 2498	. . . . . . . 8
137	135, 136	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4126	. . . . . . . 8
139	138	eleq1d 2504	. . . . . . 7
140	137, 139	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3058	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 2970	. . . . . . 7
143		vex 2970	. . . . . . 7
144	142, 143	prss 4022	. . . . . 6 $/\$
145	142	prnz 3989	. . . . . . 7
146	145	biantru 505	. . . . . 6 $/\$
147		prfi 7578	. . . . . . 7
148	147	biantru 505	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4156	. . . . . 6
151	150	eleq1i 2501	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2802	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3540	. . . 4
156	155	eleq1d 2504	. . 3
157		ineq2 3541	. . . 4
158	157	eleq1d 2504	. . 3
159	156, 158	cbvral2v 2950	. 2
160		df-3an 967	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 325	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1610	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3bitr4i 277	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wal 1367

wceq 1369

wex 1586

wcel 1756

wne 2601

wral 2710

wrex 2711

cvv 2967

cun 3321

cin 3322

wss 3323

c0 3632

csn 3872

cpr 3874

cint 4123 class class class wbr 4287

csuc 4716

ccnv 4834

crn 4836

cima 4838

wfun 5407

wfn 5408

wf 5409

wf1 5410

wfo 5411

wf1o 5412

cfv 5413

com 6471

cen 7299

cfn 7302

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 2419 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

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 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-fin 7306

This theorem is referenced by: dffi2 7665 istop2g 18484 istps4OLD 18503 neificl 28602

W3C validator