fiint - Metamath Proof Explorer

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

Theorem fiint 7793

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 7536	. . . . . . 7
2		ensym 7561	. . . . . . . . 9
3		breq1 4450	. . . . . . . . . . . . . . . 16
4	3	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1689	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4450	. . . . . . . . . . . . . . . 16
8	7	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1689	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4450	. . . . . . . . . . . . . . . 16
12	11	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1689	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7561	. . . . . . . . . . . . . . . . . . . 20
16		en0 7575	. . . . . . . . . . . . . . . . . . . 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 2664	. . . . . . . . . . . . . . . . 17
22		pm3.24 880	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 131	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 475	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1601	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1683	. . . . . . . . . . . . . . 15
29		nfa1 1845	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7522	. . . . . . . . . . . . . . . . . . 19
31		f1of 5814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4957	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 6017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5874	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4321	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5821	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5798	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4287	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2522	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 612	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1700	. . . . . . . . . . . . . . . . . . 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 1829	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6706	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1808	. . . . . . . . . . . 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 2949	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	impd 431	. . . 4 $/\$ $/\$
131	130	alrimiv 1695	. . 3 $/\$ $/\$
132		zfpair2 4687	. . . . . 6
133		sseq1 3525	. . . . . . . . 9
134		neeq1 2748	. . . . . . . . 9
135	133, 134	anbi12d 710	. . . . . . . 8 $/\$ $/\$
136		eleq1 2539	. . . . . . . 8
137	135, 136	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4285	. . . . . . . 8
139	138	eleq1d 2536	. . . . . . 7
140	137, 139	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3204	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3116	. . . . . . 7
143		vex 3116	. . . . . . 7
144	142, 143	prss 4181	. . . . . 6 $/\$
145	142	prnz 4146	. . . . . . 7
146	145	biantru 505	. . . . . 6 $/\$
147		prfi 7791	. . . . . . 7
148	147	biantru 505	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4315	. . . . . 6
151	150	eleq1i 2544	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2884	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3693	. . . 4
156	155	eleq1d 2536	. . 3
157		ineq2 3694	. . . 4
158	157	eleq1d 2536	. . 3
159	156, 158	cbvral2v 3096	. 2
160		df-3an 975	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 325	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1620	. 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 973

wal 1377

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027

cpr 4029

cint 4282 class class class wbr 4447

csuc 4880

ccnv 4998

crn 5000

cima 5002

wfun 5580

wfn 5581

wf 5582

wf1 5583

wfo 5584

wf1o 5585

cfv 5586

com 6678

cen 7510

cfn 7513

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-en 7514 df-fin 7517

This theorem is referenced by: dffi2 7879 istop2g 19172 istps4OLD 19191 neificl 29849

W3C validator