fiint - Metamath Proof Explorer

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

Theorem fiint 7789

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 7532	. . . . . . 7
2		ensym 7557	. . . . . . . . 9
3		breq1 4442	. . . . . . . . . . . . . . . 16
4	3	anbi2d 701	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 315	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1718	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4442	. . . . . . . . . . . . . . . 16
8	7	anbi2d 701	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 315	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1718	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4442	. . . . . . . . . . . . . . . 16
12	11	anbi2d 701	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 315	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1718	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7557	. . . . . . . . . . . . . . . . . . . 20
16		en0 7571	. . . . . . . . . . . . . . . . . . . 20
17	15, 16	sylib 196	. . . . . . . . . . . . . . . . . . 19
18	17	anim1i 566	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	18	ancoms 451	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	adantll 711	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		df-ne 2651	. . . . . . . . . . . . . . . . 17
22		pm3.24 880	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 131	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 473	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1623	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1712	. . . . . . . . . . . . . . 15
29		nfa1 1902	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7518	. . . . . . . . . . . . . . . . . . 19
31		f1of 5798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4946	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 6005	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3483	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 427	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2651	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
74	73	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	68, 74	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
76	75	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
77	76	exp5c 614	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	77	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
79	78	imp43 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
80	40, 79	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
81		inteq 4274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3685	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4311	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3644	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4276	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2509	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 610	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1729	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	30, 114	syl5bi 217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	imp 427	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	116	adantlr 712	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
118	117	com13 80	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
119	28, 29, 118	alrimd 1886	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6701	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1864	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
123	121, 122	syl6 33	. . . . . . . . . . 11 $/\$ $/\$
124	123	exp4a 604	. . . . . . . . . 10 $/\$
125	124	com24 87	. . . . . . . . 9 $/\$
126	2, 125	syl5 32	. . . . . . . 8 $/\$
127	126	rexlimiv 2940	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	impd 429	. . . 4 $/\$ $/\$
131	130	alrimiv 1724	. . 3 $/\$ $/\$
132		zfpair2 4677	. . . . . 6
133		sseq1 3510	. . . . . . . . 9
134		neeq1 2735	. . . . . . . . 9
135	133, 134	anbi12d 708	. . . . . . . 8 $/\$ $/\$
136		eleq1 2526	. . . . . . . 8
137	135, 136	anbi12d 708	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4274	. . . . . . . 8
139	138	eleq1d 2523	. . . . . . 7
140	137, 139	imbi12d 318	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3197	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3109	. . . . . . 7
143		vex 3109	. . . . . . 7
144	142, 143	prss 4170	. . . . . 6 $/\$
145	142	prnz 4135	. . . . . . 7
146	145	biantru 503	. . . . . 6 $/\$
147		prfi 7787	. . . . . . 7
148	147	biantru 503	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4305	. . . . . 6
151	150	eleq1i 2531	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2874	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3679	. . . 4
156	155	eleq1d 2523	. . 3
157		ineq2 3680	. . . 4
158	157	eleq1d 2523	. . 3
159	156, 158	cbvral2v 3089	. 2
160		df-3an 973	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 323	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1645	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3bitr4i 277	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wal 1396

wceq 1398

wex 1617

wcel 1823

wne 2649

wral 2804

wrex 2805

cvv 3106

cun 3459

cin 3460

wss 3461

c0 3783

csn 4016

cpr 4018

cint 4271 class class class wbr 4439

csuc 4869

ccnv 4987

crn 4989

cima 4991

wfun 5564

wfn 5565

wf 5566

wf1 5567

wfo 5568

wf1o 5569

cfv 5570

com 6673

cen 7506

cfn 7509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-en 7510 df-fin 7513

This theorem is referenced by: dffi2 7875 istop2g 19572 istps4OLD 19591 neificl 30486

W3C validator