fiintim - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > fiintim		Unicode version

Theorem fiintim 7030

Description: If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as

and

not being equal, or

having decidable equality.

This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)

**Assertion**
Ref	Expression
fiintim	$/\$ $/\$

Distinct variable group:

Proof of Theorem fiintim Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 6854	. . . . . 6
2		ensym 6875	. . . . . . . 8
3		breq1 4048	. . . . . . . . . . . . . . 15
4	3	anbi2d 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 231	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1847	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
7		breq1 4048	. . . . . . . . . . . . . . 15
8	7	anbi2d 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 231	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1847	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11		breq1 4048	. . . . . . . . . . . . . . 15
12	11	anbi2d 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 231	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1847	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		ensym 6875	. . . . . . . . . . . . . . . . . . 19
16		en0 6889	. . . . . . . . . . . . . . . . . . 19
17	15, 16	sylib 122	. . . . . . . . . . . . . . . . . 18
18	17	anim1i 340	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
19	18	ancoms 268	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20	19	adantll 476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
21		df-ne 2377	. . . . . . . . . . . . . . . 16
22		pm3.24 695	. . . . . . . . . . . . . . . . 17 $/\$
23	22	pm2.21i 647	. . . . . . . . . . . . . . . 16 $/\$
24	21, 23	sylan2b 287	. . . . . . . . . . . . . . 15 $/\$
25	20, 24	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
26	25	ax-gen 1472	. . . . . . . . . . . . 13 $/\$ $/\$
27	26	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$
28		nfv 1551	. . . . . . . . . . . . . 14 $/\$
29		nfa1 1564	. . . . . . . . . . . . . 14 $/\$ $/\$
30		simpl 109	. . . . . . . . . . . . . . . . 17 $/\$
31		bren 6837	. . . . . . . . . . . . . . . . . . 19
32		ssel 3187	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		f1of 5524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		vex 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35	34	sucid 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
36		ffvelcdm 5715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
37	33, 35, 36	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	32, 37	impel 280	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
39	38	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	adantlll 480	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		imaeq2 5019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
42		ima0 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	41, 42	eqtrdi 2254	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		inteq 3888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45		int0 3899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
46	44, 45	eqtrdi 2254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47	46	ineq1d 3373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48		ssv 3215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49		sseqin2 3392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50	48, 49	mpbi 145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
51	47, 50	eqtrdi 2254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	51	eleq1d 2274	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	biimprd 158	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		f1ofun 5526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	56	ad3antlr 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		elelsuc 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	58	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		f1odm 5528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	eleq2d 2275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62	61	ad3antlr 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	59, 62	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	jca 306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		funfvima 5818	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		ne0i 3467	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		imassrn 5034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71		dff1o2 5529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
72	71	simp3bi 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
73	70, 72	sseqtrid 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74		sstr2 3200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
76	75	anim1d 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
77		f1of1 5523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78		vex 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79		sssucid 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80		f1imaen2g 6887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
81	79, 34, 80	mpanr12 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
82	77, 78, 81	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
83	82	ensymd 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84	76, 83	jctird 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		vex 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	imaex 5038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87		sseq1 3216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88		neeq1 2389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
89	87, 88	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
90		breq2 4049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91	89, 90	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
92		inteq 3888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	92	eleq1d 2274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94	91, 93	imbi12d 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
95	86, 94	spcv 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
96	84, 95	sylan9 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
97		ineq1 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	eleq1d 2274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		ineq2 3368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	99	eleq1d 2274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	98, 100	rspc2v 2890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
102	101	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
103	96, 102	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
104	103	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
105	104	exp5c 376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
107	106	imp43 355	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	adantlll 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		0elnn 4668	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
112	111	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
113	55, 110, 112	mpjaodan 800	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	85, 34	fvex 5598	. . . . . . . . . . . . . . . . . . . . . . . . . 26
116	115	intunsn 3923	. . . . . . . . . . . . . . . . . . . . . . . . 25
117		f1ofn 5525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118		fnsnfv 5640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
119	117, 35, 118	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120	119	uneq2d 3327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121		df-suc 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122	121	imaeq2i 5021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123		imaundi 5096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	122, 123	eqtr2i 2227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	120, 124	eqtrdi 2254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 5531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 5505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	eqtrd 2238	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	inteqd 3890	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	116, 130	eqtr3id 2252	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	eleq1d 2274	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	114, 133	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp43 372	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
136	135	exlimdv 1842	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	31, 136	biimtrid 152	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138	137	expimpd 363	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	30, 138	sylani 406	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
140	139	com24 87	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
141	140	imp 124	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
142	28, 29, 141	alrimd 1633	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	ex 115	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	6, 10, 14, 27, 143	finds2 4650	. . . . . . . . . . 11 $/\$ $/\$
145		sp 1534	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
146	144, 145	syl6 33	. . . . . . . . . 10 $/\$ $/\$
147	146	exp4a 366	. . . . . . . . 9 $/\$
148	147	com24 87	. . . . . . . 8 $/\$
149	2, 148	syl5 32	. . . . . . 7 $/\$
150	149	rexlimiv 2617	. . . . . 6 $/\$
151	1, 150	sylbi 121	. . . . 5 $/\$
152	151	com13 80	. . . 4 $/\$
153	152	impd 254	. . 3 $/\$ $/\$
154	153	alrimiv 1897	. 2 $/\$ $/\$
155		ineq1 3367	. . . 4
156	155	eleq1d 2274	. . 3
157		ineq2 3368	. . . 4
158	157	eleq1d 2274	. . 3
159	156, 158	cbvral2v 2751	. 2
160		df-3an 983	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 238	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1493	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3imtr4i 201	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 $/\$ w3a 981

wal 1371

wceq 1373

wex 1515

wcel 2176

wne 2376

wral 2484

wrex 2485

cvv 2772

cun 3164

cin 3165

wss 3166

c0 3460

csn 3633

cint 3885 class class class wbr 4045

csuc 4413

com 4639

ccnv 4675

cdm 4676

crn 4677

cima 4679

wfun 5266

wfn 5267

wf 5268

wf1 5269

wfo 5270

wf1o 5271

cfv 5272

cen 6827

cfn 6829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-iinf 4637

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-ral 2489 df-rex 2490 df-v 2774 df-sbc 2999 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-br 4046 df-opab 4107 df-id 4341 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-er 6622 df-en 6830 df-fin 6832

This theorem is referenced by: istopfin 14505

W3C validator