fiintim - Intuitionistic Logic Explorer

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

Theorem fiintim 6894

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 6727	. . . . . 6
2		ensym 6747	. . . . . . . 8
3		breq1 3985	. . . . . . . . . . . . . . 15
4	3	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1812	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
7		breq1 3985	. . . . . . . . . . . . . . 15
8	7	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1812	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11		breq1 3985	. . . . . . . . . . . . . . 15
12	11	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1812	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		ensym 6747	. . . . . . . . . . . . . . . . . . 19
16		en0 6761	. . . . . . . . . . . . . . . . . . 19
17	15, 16	sylib 121	. . . . . . . . . . . . . . . . . 18
18	17	anim1i 338	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
19	18	ancoms 266	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20	19	adantll 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
21		df-ne 2337	. . . . . . . . . . . . . . . 16
22		pm3.24 683	. . . . . . . . . . . . . . . . 17 $/\$
23	22	pm2.21i 636	. . . . . . . . . . . . . . . 16 $/\$
24	21, 23	sylan2b 285	. . . . . . . . . . . . . . 15 $/\$
25	20, 24	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
26	25	ax-gen 1437	. . . . . . . . . . . . 13 $/\$ $/\$
27	26	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$
28		nfv 1516	. . . . . . . . . . . . . 14 $/\$
29		nfa1 1529	. . . . . . . . . . . . . 14 $/\$ $/\$
30		simpl 108	. . . . . . . . . . . . . . . . 17 $/\$
31		bren 6713	. . . . . . . . . . . . . . . . . . 19
32		ssel 3136	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		f1of 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35	34	sucid 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
36		ffvelrn 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
37	33, 35, 36	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	32, 37	impel 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
39	38	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	adantlll 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		imaeq2 4942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
42		ima0 4963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	41, 42	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		inteq 3827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45		int0 3838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
46	44, 45	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47	46	ineq1d 3322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48		ssv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49		sseqin2 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
51	47, 50	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	51	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		f1ofun 5434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	56	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		elelsuc 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	58	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		f1odm 5436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	eleq2d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62	61	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	jca 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		funfvima 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		ne0i 3415	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		imassrn 4957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71		dff1o2 5437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
72	71	simp3bi 1004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
73	70, 72	sseqtrid 3192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74		sstr2 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
76	75	anim1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
77		f1of1 5431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79		sssucid 4393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80		f1imaen2g 6759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
81	79, 34, 80	mpanr12 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
82	77, 78, 81	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
83	82	ensymd 6749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84	76, 83	jctird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		vex 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	imaex 4959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87		sseq1 3165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88		neeq1 2349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
89	87, 88	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
90		breq2 3986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91	89, 90	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
92		inteq 3827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	92	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
95	86, 94	spcv 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
96	84, 95	sylan9 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
97		ineq1 3316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		ineq2 3317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	99	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	98, 100	rspc2v 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
102	101	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
103	96, 102	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
104	103	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
105	104	exp5c 374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
107	106	imp43 353	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	adantlll 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		0elnn 4596	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
112	111	ad3antrrr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
113	55, 110, 112	mpjaodan 788	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	85, 34	fvex 5506	. . . . . . . . . . . . . . . . . . . . . . . . . 26
116	115	intunsn 3862	. . . . . . . . . . . . . . . . . . . . . . . . 25
117		f1ofn 5433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118		fnsnfv 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
119	117, 35, 118	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120	119	uneq2d 3276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121		df-suc 4349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122	121	imaeq2i 4944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123		imaundi 5016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	122, 123	eqtr2i 2187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	120, 124	eqtrdi 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 5439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 5415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	eqtrd 2198	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	inteqd 3829	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	116, 130	eqtr3id 2213	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	eleq1d 2235	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ad2antlr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp43 370	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
136	135	exlimdv 1807	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	31, 136	syl5bi 151	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138	137	expimpd 361	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	30, 138	sylani 404	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
140	139	com24 87	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
141	140	imp 123	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
142	28, 29, 141	alrimd 1598	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	ex 114	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	6, 10, 14, 27, 143	finds2 4578	. . . . . . . . . . 11 $/\$ $/\$
145		sp 1499	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
146	144, 145	syl6 33	. . . . . . . . . 10 $/\$ $/\$
147	146	exp4a 364	. . . . . . . . 9 $/\$
148	147	com24 87	. . . . . . . 8 $/\$
149	2, 148	syl5 32	. . . . . . 7 $/\$
150	149	rexlimiv 2577	. . . . . 6 $/\$
151	1, 150	sylbi 120	. . . . 5 $/\$
152	151	com13 80	. . . 4 $/\$
153	152	impd 252	. . 3 $/\$ $/\$
154	153	alrimiv 1862	. 2 $/\$ $/\$
155		ineq1 3316	. . . 4
156	155	eleq1d 2235	. . 3
157		ineq2 3317	. . . 4
158	157	eleq1d 2235	. . 3
159	156, 158	cbvral2v 2705	. 2
160		df-3an 970	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 237	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1458	. 2 $/\$ $/\$ $/\$ $/\$
163	154, 159, 162	3imtr4i 200	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698 $/\$ w3a 968

wal 1341

wceq 1343

wex 1480

wcel 2136

wne 2336

wral 2444

wrex 2445

cvv 2726

cun 3114

cin 3115

wss 3116

c0 3409

csn 3576

cint 3824 class class class wbr 3982

csuc 4343

com 4567

ccnv 4603

cdm 4604

crn 4605

cima 4607

wfun 5182

wfn 5183

wf 5184

wf1 5185

wfo 5186

wf1o 5187

cfv 5188

cen 6704

cfn 6706

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-iinf 4565

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-v 2728 df-sbc 2952 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-br 3983 df-opab 4044 df-id 4271 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-er 6501 df-en 6707 df-fin 6709

This theorem is referenced by: istopfin 12638

W3C validator