fiint - Metamath Proof Explorer

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

Theorem fiint 7576

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 7321	. . . . . . 7
2		ensym 7346	. . . . . . . . 9
3		breq1 4283	. . . . . . . . . . . . . . . 16
4	3	anbi2d 696	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1678	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4283	. . . . . . . . . . . . . . . 16
8	7	anbi2d 696	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1678	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4283	. . . . . . . . . . . . . . . 16
12	11	anbi2d 696	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1678	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7346	. . . . . . . . . . . . . . . . . . . 20
16		en0 7360	. . . . . . . . . . . . . . . . . . . 20
17	15, 16	sylib 196	. . . . . . . . . . . . . . . . . . 19
18	17	anim1i 563	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	18	ancoms 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	adantll 706	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		df-ne 2598	. . . . . . . . . . . . . . . . 17
22		pm3.24 870	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 131	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 472	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1594	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1672	. . . . . . . . . . . . . . 15
29		nfa1 1829	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7307	. . . . . . . . . . . . . . . . . . 19
31		f1of 5629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 655	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3338	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2598	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
74	73	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	68, 74	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
76	75	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
77	76	exp5c 611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	77	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
79	78	imp43 590	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
80	40, 79	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
81		inteq 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3364	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2499	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4155	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4121	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2479	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2499	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 719	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 607	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1689	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	30, 114	syl5bi 217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	imp 429	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	116	adantlr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
118	117	com13 80	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
119	28, 29, 118	alrimd 1814	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6493	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1793	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
123	121, 122	syl6 33	. . . . . . . . . . 11 $/\$ $/\$
124	123	exp4a 601	. . . . . . . . . 10 $/\$
125	124	com24 87	. . . . . . . . 9 $/\$
126	2, 125	syl5 32	. . . . . . . 8 $/\$
127	126	rexlimiv 2825	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	imp3a 431	. . . 4 $/\$ $/\$
131	130	alrimiv 1684	. . 3 $/\$ $/\$
132		zfpair2 4520	. . . . . 6
133		sseq1 3365	. . . . . . . . 9
134		neeq1 2606	. . . . . . . . 9
135	133, 134	anbi12d 703	. . . . . . . 8 $/\$ $/\$
136		eleq1 2493	. . . . . . . 8
137	135, 136	anbi12d 703	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4119	. . . . . . . 8
139	138	eleq1d 2499	. . . . . . 7
140	137, 139	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3052	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 2965	. . . . . . 7
143		vex 2965	. . . . . . 7
144	142, 143	prss 4015	. . . . . 6 $/\$
145	142	prnz 3982	. . . . . . 7
146	145	biantru 502	. . . . . 6 $/\$
147		prfi 7574	. . . . . . 7
148	147	biantru 502	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4149	. . . . . 6
151	150	eleq1i 2496	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2797	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3533	. . . 4
156	155	eleq1d 2499	. . 3
157		ineq2 3534	. . . 4
158	157	eleq1d 2499	. . 3
159	156, 158	cbvral2v 2945	. 2
160		df-3an 960	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 325	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1613	. 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 958

wal 1360

wceq 1362

wex 1589

wcel 1755

wne 2596

wral 2705

wrex 2706

cvv 2962

cun 3314

cin 3315

wss 3316

c0 3625

csn 3865

cpr 3867

cint 4116 class class class wbr 4280

csuc 4708

ccnv 4826

crn 4828

cima 4830

wfun 5400

wfn 5401

wf 5402

wf1 5403

wfo 5404

wf1o 5405

cfv 5406

com 6465

cen 7295

cfn 7298

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-ral 2710 df-rex 2711 df-reu 2712 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-en 7299 df-fin 7302

This theorem is referenced by: dffi2 7661 istop2g 18350 istps4OLD 18369 neificl 28490

W3C validator