fiint - Metamath Proof Explorer

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

Theorem fiint 7692

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 7436	. . . . . . 7
2		ensym 7461	. . . . . . . . 9
3		breq1 4396	. . . . . . . . . . . . . . . 16
4	3	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1680	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4396	. . . . . . . . . . . . . . . 16
8	7	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1680	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4396	. . . . . . . . . . . . . . . 16
12	11	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1680	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7461	. . . . . . . . . . . . . . . . . . . 20
16		en0 7475	. . . . . . . . . . . . . . . . . . . 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 2646	. . . . . . . . . . . . . . . . 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 1592	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1674	. . . . . . . . . . . . . . 15
29		nfa1 1833	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7422	. . . . . . . . . . . . . . . . . . 19
31		f1of 5742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4899	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 5943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3451	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2646	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3670	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2520	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5802	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4268	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2492	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4234	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2520	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 612	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1691	. . . . . . . . . . . . . . . . . . 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 1817	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6607	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1796	. . . . . . . . . . . 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 2934	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	impd 431	. . . 4 $/\$ $/\$
131	130	alrimiv 1686	. . 3 $/\$ $/\$
132		zfpair2 4633	. . . . . 6
133		sseq1 3478	. . . . . . . . 9
134		neeq1 2729	. . . . . . . . 9
135	133, 134	anbi12d 710	. . . . . . . 8 $/\$ $/\$
136		eleq1 2523	. . . . . . . 8
137	135, 136	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4232	. . . . . . . 8
139	138	eleq1d 2520	. . . . . . 7
140	137, 139	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3162	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3074	. . . . . . 7
143		vex 3074	. . . . . . 7
144	142, 143	prss 4128	. . . . . 6 $/\$
145	142	prnz 4095	. . . . . . 7
146	145	biantru 505	. . . . . 6 $/\$
147		prfi 7690	. . . . . . 7
148	147	biantru 505	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4262	. . . . . 6
151	150	eleq1i 2528	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2906	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3646	. . . 4
156	155	eleq1d 2520	. . 3
157		ineq2 3647	. . . 4
158	157	eleq1d 2520	. . 3
159	156, 158	cbvral2v 3054	. 2
160		df-3an 967	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 325	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1611	. 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 1368

wceq 1370

wex 1587

wcel 1758

wne 2644

wral 2795

wrex 2796

cvv 3071

cun 3427

cin 3428

wss 3429

c0 3738

csn 3978

cpr 3980

cint 4229 class class class wbr 4393

csuc 4822

ccnv 4940

crn 4942

cima 4944

wfun 5513

wfn 5514

wf 5515

wf1 5516

wfo 5517

wf1o 5518

cfv 5519

com 6579

cen 7410

cfn 7413

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-om 6580 df-recs 6935 df-rdg 6969 df-1o 7023 df-oadd 7027 df-er 7204 df-en 7414 df-fin 7417

This theorem is referenced by: dffi2 7777 istop2g 18634 istps4OLD 18653 neificl 28790

W3C validator