fiint - Metamath Proof Explorer

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

Theorem fiint 7848

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 7593	. . . . . . 7
2		ensym 7618	. . . . . . . . 9
3		breq1 4405	. . . . . . . . . . . . . . . 16
4	3	anbi2d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1767	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
7		breq1 4405	. . . . . . . . . . . . . . . 16
8	7	anbi2d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1767	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11		breq1 4405	. . . . . . . . . . . . . . . 16
12	11	anbi2d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1767	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15		ensym 7618	. . . . . . . . . . . . . . . . . . . 20
16		en0 7632	. . . . . . . . . . . . . . . . . . . 20
17	15, 16	sylib 200	. . . . . . . . . . . . . . . . . . 19
18	17	anim1i 572	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	18	ancoms 455	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	adantll 720	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		df-ne 2624	. . . . . . . . . . . . . . . . 17
22		pm3.24 893	. . . . . . . . . . . . . . . . . 18 $/\$
23	22	pm2.21i 135	. . . . . . . . . . . . . . . . 17 $/\$
24	21, 23	sylan2b 478	. . . . . . . . . . . . . . . 16 $/\$
25	20, 24	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	ax-gen 1669	. . . . . . . . . . . . . 14 $/\$ $/\$
27	26	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
28		nfv 1761	. . . . . . . . . . . . . . 15
29		nfa1 1979	. . . . . . . . . . . . . . 15 $/\$ $/\$
30		bren 7578	. . . . . . . . . . . . . . . . . . 19
31		f1of 5814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
32		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
33	32	sucid 5502	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		ffvelrn 6020	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35	31, 33, 34	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36		ssel 3426	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37	35, 36	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	37	imp 431	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
40		df-ne 2624	. . . . . . . . . . . . . . . . . . . . . . . . 25
41		imassrn 5179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42		dff1o2 5819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
43	42	simp3bi 1025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
44	41, 43	syl5sseq 3480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45		sstr2 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
47	46	anim1d 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
48		f1of1 5813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50		sssucid 5500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		f1imaen2g 7630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
52	50, 32, 51	mpanr12 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
53	48, 49, 52	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
54	53	ensymd 7620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
55	47, 54	jctird 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
56		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57		imaexg 6730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
58	56, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		sseq1 3453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60		neeq1 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	59, 60	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
62		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
64		inteq 4237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
65	64	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	63, 65	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
67	58, 66	spcv 3140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
68	55, 67	sylan9 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
69		ineq1 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		ineq2 3628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	rspc2v 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
74	73	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	68, 74	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
76	75	com4r 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
77	76	exp5c 621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
78	77	com14 91	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
79	78	imp43 600	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
80	40, 79	syl5bir 222	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
81		inteq 4237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82		int0 4248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	81, 82	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	ineq1d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85		ssv 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		sseqin2 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87	85, 86	mpbi 212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	84, 87	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	88	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	biimprd 227	. . . . . . . . . . . . . . . . . . . . . . . 24
91	80, 90	pm2.61d2 164	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
92	39, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
93		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94	93	intunsn 4274	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		f1ofn 5815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		fnsnfv 5925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
97	95, 33, 96	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	uneq2d 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		df-suc 5429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	99	imaeq2i 5166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		imaundi 5248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	eqtr2i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	98, 102	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104		f1ofo 5821	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105		foima 5798	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	103, 106	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	inteqd 4239	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	94, 108	syl5eqr 2499	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . 23
111	110	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	92, 111	mpbid 214	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	exp43 617	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	exlimdv 1779	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	30, 114	syl5bi 221	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	imp 431	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	116	adantlr 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
118	117	com13 83	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
119	28, 29, 118	alrimd 1959	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
120	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	6, 10, 14, 27, 120	finds2 6721	. . . . . . . . . . . 12 $/\$ $/\$
122		sp 1937	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
123	121, 122	syl6 34	. . . . . . . . . . 11 $/\$ $/\$
124	123	exp4a 611	. . . . . . . . . 10 $/\$
125	124	com24 90	. . . . . . . . 9 $/\$
126	2, 125	syl5 33	. . . . . . . 8 $/\$
127	126	rexlimiv 2873	. . . . . . 7 $/\$
128	1, 127	sylbi 199	. . . . . 6 $/\$
129	128	com13 83	. . . . 5 $/\$
130	129	impd 433	. . . 4 $/\$ $/\$
131	130	alrimiv 1773	. . 3 $/\$ $/\$
132		zfpair2 4640	. . . . . 6
133		sseq1 3453	. . . . . . . . 9
134		neeq1 2686	. . . . . . . . 9
135	133, 134	anbi12d 717	. . . . . . . 8 $/\$ $/\$
136		eleq1 2517	. . . . . . . 8
137	135, 136	anbi12d 717	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
138		inteq 4237	. . . . . . . 8
139	138	eleq1d 2513	. . . . . . 7
140	137, 139	imbi12d 322	. . . . . 6 $/\$ $/\$ $/\$ $/\$
141	132, 140	spcv 3140	. . . . 5 $/\$ $/\$ $/\$ $/\$
142		vex 3048	. . . . . . 7
143		vex 3048	. . . . . . 7
144	142, 143	prss 4126	. . . . . 6 $/\$
145	142	prnz 4091	. . . . . . 7
146	145	biantru 508	. . . . . 6 $/\$
147		prfi 7846	. . . . . . 7
148	147	biantru 508	. . . . . 6 $/\$ $/\$ $/\$
149	144, 146, 148	3bitrri 276	. . . . 5 $/\$ $/\$ $/\$
150	142, 143	intpr 4268	. . . . . 6
151	150	eleq1i 2520	. . . . 5
152	141, 149, 151	3imtr3g 273	. . . 4 $/\$ $/\$ $/\$
153	152	ralrimivv 2808	. . 3 $/\$ $/\$
154	131, 153	impbii 191	. 2 $/\$ $/\$
155		ineq1 3627	. . . 4
156	155	eleq1d 2513	. . 3
157		ineq2 3628	. . . 4
158	157	eleq1d 2513	. . 3
159	156, 158	cbvral2v 3027	. 2
160		df-3an 987	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 327	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1691	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3bitr4i 281	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wal 1442

wceq 1444

wex 1663

wcel 1887

wne 2622

wral 2737

wrex 2738

cvv 3045

cun 3402

cin 3403

wss 3404

c0 3731

csn 3968

cpr 3970

cint 4234 class class class wbr 4402

ccnv 4833

crn 4835

cima 4837

csuc 5425

wfun 5576

wfn 5577

wf 5578

wf1 5579

wfo 5580

wf1o 5581

cfv 5582

com 6692

cen 7566

cfn 7569

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-fin 7573

This theorem is referenced by: dffi2 7937 istop2g 19926 neificl 32082

W3C validator