fiint - Metamath Proof Explorer

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

Theorem fiint 7796

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 7538	. . . . . . 7
2		ensym 7563	. . . . . . . . 9
3		breq1 4437	. . . . . . . . . . . . . . . 16
4	3	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1698	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4437	. . . . . . . . . . . . . . . 16
8	7	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1698	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4437	. . . . . . . . . . . . . . . 16
12	11	anbi2d 703	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 317	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1698	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7563	. . . . . . . . . . . . . . . . . . . 20
16		en0 7577	. . . . . . . . . . . . . . . . . . . 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 2638	. . . . . . . . . . . . . . . . 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 1603	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1692	. . . . . . . . . . . . . . 15
29		nfa1 1881	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7524	. . . . . . . . . . . . . . . . . . 19
31		f1of 5803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 4944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 6011	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3481	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2638	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 4942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3700	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2510	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5863	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4308	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 4871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5810	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4273	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2496	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2510	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 612	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1709	. . . . . . . . . . . . . . . . . . 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 1865	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6710	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1843	. . . . . . . . . . . 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 2927	. . . . . . 7 $/\$
128	1, 127	sylbi 195	. . . . . 6 $/\$
129	128	com13 80	. . . . 5 $/\$
130	129	impd 431	. . . 4 $/\$ $/\$
131	130	alrimiv 1704	. . 3 $/\$ $/\$
132		zfpair2 4674	. . . . . 6
133		sseq1 3508	. . . . . . . . 9
134		neeq1 2722	. . . . . . . . 9
135	133, 134	anbi12d 710	. . . . . . . 8 $/\$ $/\$
136		eleq1 2513	. . . . . . . 8
137	135, 136	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4271	. . . . . . . 8
139	138	eleq1d 2510	. . . . . . 7
140	137, 139	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3184	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3096	. . . . . . 7
143		vex 3096	. . . . . . 7
144	142, 143	prss 4166	. . . . . 6 $/\$
145	142	prnz 4131	. . . . . . 7
146	145	biantru 505	. . . . . 6 $/\$
147		prfi 7794	. . . . . . 7
148	147	biantru 505	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 272	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4302	. . . . . 6
151	150	eleq1i 2518	. . . . 5
152	141, 149, 151	3imtr3g 269	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2861	. . 3 $/\$ $/\$
154	131, 153	impbii 188	. 2 $/\$ $/\$
155		ineq1 3676	. . . 4
156	155	eleq1d 2510	. . 3
157		ineq2 3677	. . . 4
158	157	eleq1d 2510	. . 3
159	156, 158	cbvral2v 3076	. 2
160		df-3an 974	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 325	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1625	. 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 972

wal 1379

wceq 1381

wex 1597

wcel 1802

wne 2636

wral 2791

wrex 2792

cvv 3093

cun 3457

cin 3458

wss 3459

c0 3768

csn 4011

cpr 4013

cint 4268 class class class wbr 4434

csuc 4867

ccnv 4985

crn 4987

cima 4989

wfun 5569

wfn 5570

wf 5571

wf1 5572

wfo 5573

wf1o 5574

cfv 5575

com 6682

cen 7512

cfn 7515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-sep 4555 ax-nul 4563 ax-pow 4612 ax-pr 4673 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-ral 2796 df-rex 2797 df-reu 2798 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3419 df-dif 3462 df-un 3464 df-in 3466 df-ss 3473 df-pss 3475 df-nul 3769 df-if 3924 df-pw 3996 df-sn 4012 df-pr 4014 df-tp 4016 df-op 4018 df-uni 4232 df-int 4269 df-iun 4314 df-br 4435 df-opab 4493 df-mpt 4494 df-tr 4528 df-eprel 4778 df-id 4782 df-po 4787 df-so 4788 df-fr 4825 df-we 4827 df-ord 4868 df-on 4869 df-lim 4870 df-suc 4871 df-xp 4992 df-rel 4993 df-cnv 4994 df-co 4995 df-dm 4996 df-rn 4997 df-res 4998 df-ima 4999 df-iota 5538 df-fun 5577 df-fn 5578 df-f 5579 df-f1 5580 df-fo 5581 df-f1o 5582 df-fv 5583 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6683 df-recs 7041 df-rdg 7075 df-1o 7129 df-oadd 7133 df-er 7310 df-en 7516 df-fin 7519

This theorem is referenced by: dffi2 7882 istop2g 19275 istps4OLD 19294 neificl 30218

W3C validator