fiintim - Intuitionistic Logic Explorer

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

Theorem fiintim 6906

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 6739	. . . . . 6
2		ensym 6759	. . . . . . . 8
3		breq1 3992	. . . . . . . . . . . . . . 15
4	3	anbi2d 461	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1817	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
7		breq1 3992	. . . . . . . . . . . . . . 15
8	7	anbi2d 461	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1817	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11		breq1 3992	. . . . . . . . . . . . . . 15
12	11	anbi2d 461	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1817	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		ensym 6759	. . . . . . . . . . . . . . . . . . 19
16		en0 6773	. . . . . . . . . . . . . . . . . . 19
17	15, 16	sylib 121	. . . . . . . . . . . . . . . . . 18
18	17	anim1i 338	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
19	18	ancoms 266	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20	19	adantll 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
21		df-ne 2341	. . . . . . . . . . . . . . . 16
22		pm3.24 688	. . . . . . . . . . . . . . . . 17 $/\$
23	22	pm2.21i 641	. . . . . . . . . . . . . . . 16 $/\$
24	21, 23	sylan2b 285	. . . . . . . . . . . . . . 15 $/\$
25	20, 24	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
26	25	ax-gen 1442	. . . . . . . . . . . . 13 $/\$ $/\$
27	26	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$
28		nfv 1521	. . . . . . . . . . . . . 14 $/\$
29		nfa1 1534	. . . . . . . . . . . . . 14 $/\$ $/\$
30		simpl 108	. . . . . . . . . . . . . . . . 17 $/\$
31		bren 6725	. . . . . . . . . . . . . . . . . . 19
32		ssel 3141	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		f1of 5442	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		vex 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35	34	sucid 4402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
36		ffvelrn 5629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
37	33, 35, 36	sylancl 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	32, 37	impel 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
39	38	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	adantlll 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		imaeq2 4949	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
42		ima0 4970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	41, 42	eqtrdi 2219	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		inteq 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45		int0 3845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
46	44, 45	eqtrdi 2219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47	46	ineq1d 3327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48		ssv 3169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49		sseqin2 3346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
51	47, 50	eqtrdi 2219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	51	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		f1ofun 5444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	56	ad3antlr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		elelsuc 4394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	58	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		f1odm 5446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	eleq2d 2240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62	61	ad3antlr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	jca 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		funfvima 5727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		ne0i 3421	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		imassrn 4964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71		dff1o2 5447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
72	71	simp3bi 1009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
73	70, 72	sseqtrid 3197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74		sstr2 3154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
76	75	anim1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
77		f1of1 5441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78		vex 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79		sssucid 4400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80		f1imaen2g 6771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
81	79, 34, 80	mpanr12 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
82	77, 78, 81	sylancl 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
83	82	ensymd 6761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84	76, 83	jctird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		vex 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	imaex 4966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87		sseq1 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88		neeq1 2353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
89	87, 88	anbi12d 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
90		breq2 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91	89, 90	anbi12d 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
92		inteq 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	92	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
95	86, 94	spcv 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
96	84, 95	sylan9 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
97		ineq1 3321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		ineq2 3322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	99	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	98, 100	rspc2v 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		0elnn 4603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
112	111	ad3antrrr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
113	55, 110, 112	mpjaodan 793	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	85, 34	fvex 5516	. . . . . . . . . . . . . . . . . . . . . . . . . 26
116	115	intunsn 3869	. . . . . . . . . . . . . . . . . . . . . . . . 25
117		f1ofn 5443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118		fnsnfv 5555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
119	117, 35, 118	sylancl 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120	119	uneq2d 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121		df-suc 4356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122	121	imaeq2i 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123		imaundi 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	122, 123	eqtr2i 2192	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	120, 124	eqtrdi 2219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 5425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	eqtrd 2203	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	inteqd 3836	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	116, 130	eqtr3id 2217	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ad2antlr 486	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp43 370	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
136	135	exlimdv 1812	. . . . . . . . . . . . . . . . . . 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 1603	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	ex 114	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	6, 10, 14, 27, 143	finds2 4585	. . . . . . . . . . 11 $/\$ $/\$
145		sp 1504	. . . . . . . . . . 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 2581	. . . . . 6 $/\$
151	1, 150	sylbi 120	. . . . 5 $/\$
152	151	com13 80	. . . 4 $/\$
153	152	impd 252	. . 3 $/\$ $/\$
154	153	alrimiv 1867	. 2 $/\$ $/\$
155		ineq1 3321	. . . 4
156	155	eleq1d 2239	. . 3
157		ineq2 3322	. . . 4
158	157	eleq1d 2239	. . 3
159	156, 158	cbvral2v 2709	. 2
160		df-3an 975	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 237	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1463	. 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 703 $/\$ w3a 973

wal 1346

wceq 1348

wex 1485

wcel 2141

wne 2340

wral 2448

wrex 2449

cvv 2730

cun 3119

cin 3120

wss 3121

c0 3414

csn 3583

cint 3831 class class class wbr 3989

csuc 4350

com 4574

ccnv 4610

cdm 4611

crn 4612

cima 4614

wfun 5192

wfn 5193

wf 5194

wf1 5195

wfo 5196

wf1o 5197

cfv 5198

cen 6716

cfn 6718

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-iinf 4572

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-ral 2453 df-rex 2454 df-v 2732 df-sbc 2956 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-br 3990 df-opab 4051 df-id 4278 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-er 6513 df-en 6719 df-fin 6721

This theorem is referenced by: istopfin 12792

W3C validator