fiint - Metamath Proof Explorer

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

Theorem fiint 7845

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 7591	. . . . . . 7
2		ensym 7616	. . . . . . . . 9
3		breq1 4420	. . . . . . . . . . . . . . . 16
4	3	anbi2d 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 318	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1757	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4420	. . . . . . . . . . . . . . . 16
8	7	anbi2d 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 318	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1757	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4420	. . . . . . . . . . . . . . . 16
12	11	anbi2d 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 318	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1757	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7616	. . . . . . . . . . . . . . . . . . . 20
16		en0 7630	. . . . . . . . . . . . . . . . . . . 20
17	15, 16	sylib 199	. . . . . . . . . . . . . . . . . . 19
18	17	anim1i 570	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	18	ancoms 454	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	adantll 718	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		df-ne 2618	. . . . . . . . . . . . . . . . 17
22		pm3.24 890	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 134	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 477	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1665	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1751	. . . . . . . . . . . . . . 15
29		nfa1 1951	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7577	. . . . . . . . . . . . . . . . . . 19
31		f1of 5822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 5512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 6026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3455	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2618	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 5510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
74	73	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	68, 74	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
76	75	com4r 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
77	76	exp5c 619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	77	com14 91	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
79	78	imp43 598	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
80	40, 79	syl5bir 221	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
81		inteq 4252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2489	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 226	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 163	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5882	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4289	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 5439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4254	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2475	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2489	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 615	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	30, 114	syl5bi 220	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	imp 430	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	116	adantlr 719	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
118	117	com13 83	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
119	28, 29, 118	alrimd 1931	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6726	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1909	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
123	121, 122	syl6 34	. . . . . . . . . . 11 $/\$ $/\$
124	123	exp4a 609	. . . . . . . . . 10 $/\$
125	124	com24 90	. . . . . . . . 9 $/\$
126	2, 125	syl5 33	. . . . . . . 8 $/\$
127	126	rexlimiv 2909	. . . . . . 7 $/\$
128	1, 127	sylbi 198	. . . . . 6 $/\$
129	128	com13 83	. . . . 5 $/\$
130	129	impd 432	. . . 4 $/\$ $/\$
131	130	alrimiv 1763	. . 3 $/\$ $/\$
132		zfpair2 4653	. . . . . 6
133		sseq1 3482	. . . . . . . . 9
134		neeq1 2703	. . . . . . . . 9
135	133, 134	anbi12d 715	. . . . . . . 8 $/\$ $/\$
136		eleq1 2492	. . . . . . . 8
137	135, 136	anbi12d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4252	. . . . . . . 8
139	138	eleq1d 2489	. . . . . . 7
140	137, 139	imbi12d 321	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3169	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3081	. . . . . . 7
143		vex 3081	. . . . . . 7
144	142, 143	prss 4148	. . . . . 6 $/\$
145	142	prnz 4113	. . . . . . 7
146	145	biantru 507	. . . . . 6 $/\$
147		prfi 7843	. . . . . . 7
148	147	biantru 507	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 275	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4283	. . . . . 6
151	150	eleq1i 2497	. . . . 5
152	141, 149, 151	3imtr3g 272	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2843	. . 3 $/\$ $/\$
154	131, 153	impbii 190	. 2 $/\$ $/\$
155		ineq1 3654	. . . 4
156	155	eleq1d 2489	. . 3
157		ineq2 3655	. . . 4
158	157	eleq1d 2489	. . 3
159	156, 158	cbvral2v 3061	. 2
160		df-3an 984	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 326	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1687	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3bitr4i 280	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wal 1435

wceq 1437

wex 1659

wcel 1867

wne 2616

wral 2773

wrex 2774

cvv 3078

cun 3431

cin 3432

wss 3433

c0 3758

csn 3993

cpr 3995

cint 4249 class class class wbr 4417

ccnv 4844

crn 4846

cima 4848

csuc 5435

wfun 5586

wfn 5587

wf 5588

wf1 5589

wfo 5590

wf1o 5591

cfv 5592

com 6697

cen 7565

cfn 7568

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-ral 2778 df-rex 2779 df-reu 2780 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-oadd 7185 df-er 7362 df-en 7569 df-fin 7572

This theorem is referenced by: dffi2 7934 istop2g 19850 neificl 31786

W3C validator