fiintim - Intuitionistic Logic Explorer

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

Theorem fiintim 6810

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 6648	. . . . . 6
2		ensym 6668	. . . . . . . 8
3		breq1 3927	. . . . . . . . . . . . . . 15
4	3	anbi2d 459	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1796	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
7		breq1 3927	. . . . . . . . . . . . . . 15
8	7	anbi2d 459	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1796	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11		breq1 3927	. . . . . . . . . . . . . . 15
12	11	anbi2d 459	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1796	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		ensym 6668	. . . . . . . . . . . . . . . . . . 19
16		en0 6682	. . . . . . . . . . . . . . . . . . 19
17	15, 16	sylib 121	. . . . . . . . . . . . . . . . . 18
18	17	anim1i 338	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
19	18	ancoms 266	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20	19	adantll 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
21		df-ne 2307	. . . . . . . . . . . . . . . 16
22		pm3.24 682	. . . . . . . . . . . . . . . . 17 $/\$
23	22	pm2.21i 635	. . . . . . . . . . . . . . . 16 $/\$
24	21, 23	sylan2b 285	. . . . . . . . . . . . . . 15 $/\$
25	20, 24	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
26	25	ax-gen 1425	. . . . . . . . . . . . 13 $/\$ $/\$
27	26	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$
28		nfv 1508	. . . . . . . . . . . . . 14 $/\$
29		nfa1 1521	. . . . . . . . . . . . . 14 $/\$ $/\$
30		simpl 108	. . . . . . . . . . . . . . . . 17 $/\$
31		bren 6634	. . . . . . . . . . . . . . . . . . 19
32		ssel 3086	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		f1of 5360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		vex 2684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35	34	sucid 4334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
36		ffvelrn 5546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
37	33, 35, 36	sylancl 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	32, 37	impel 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
39	38	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	adantlll 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		imaeq2 4872	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
42		ima0 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	41, 42	syl6eq 2186	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		inteq 3769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45		int0 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
46	44, 45	syl6eq 2186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47	46	ineq1d 3271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48		ssv 3114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49		sseqin2 3290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
51	47, 50	syl6eq 2186	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	51	eleq1d 2206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		f1ofun 5362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	56	ad3antlr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		elelsuc 4326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	58	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		f1odm 5364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	eleq2d 2207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62	61	ad3antlr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	jca 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		funfvima 5642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		ne0i 3364	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		imassrn 4887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71		dff1o2 5365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
72	71	simp3bi 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
73	70, 72	sseqtrid 3142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74		sstr2 3099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
76	75	anim1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
77		f1of1 5359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78		vex 2684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79		sssucid 4332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80		f1imaen2g 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
81	79, 34, 80	mpanr12 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
82	77, 78, 81	sylancl 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
83	82	ensymd 6670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84	76, 83	jctird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		vex 2684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	imaex 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87		sseq1 3115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88		neeq1 2319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
89	87, 88	anbi12d 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
90		breq2 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91	89, 90	anbi12d 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
92		inteq 3769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	92	eleq1d 2206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
95	86, 94	spcv 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
96	84, 95	sylan9 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
97		ineq1 3265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	eleq1d 2206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		ineq2 3266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	99	eleq1d 2206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	98, 100	rspc2v 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
102	101	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
103	96, 102	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
104	103	com4r 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
105	104	exp5c 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
106	105	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
107	106	imp43 352	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	adantlll 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	adantr 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	69, 109	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		0elnn 4527	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
112	111	ad3antrrr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
113	55, 110, 112	mpjaodan 787	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	85, 34	fvex 5434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
116	115	intunsn 3804	. . . . . . . . . . . . . . . . . . . . . . . . 25
117		f1ofn 5361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118		fnsnfv 5473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
119	117, 35, 118	sylancl 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120	119	uneq2d 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121		df-suc 4288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122	121	imaeq2i 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123		imaundi 4946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	122, 123	eqtr2i 2159	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	120, 124	syl6eq 2186	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 5367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 5345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	eqtrd 2170	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	inteqd 3771	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	116, 130	syl5eqr 2184	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	eleq1d 2206	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ad2antlr 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp43 369	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
136	135	exlimdv 1791	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	31, 136	syl5bi 151	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138	137	expimpd 360	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	30, 138	sylani 403	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
140	139	com24 87	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
141	140	imp 123	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
142	28, 29, 141	alrimd 1589	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	ex 114	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	6, 10, 14, 27, 143	finds2 4510	. . . . . . . . . . 11 $/\$ $/\$
145		sp 1488	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
146	144, 145	syl6 33	. . . . . . . . . 10 $/\$ $/\$
147	146	exp4a 363	. . . . . . . . 9 $/\$
148	147	com24 87	. . . . . . . 8 $/\$
149	2, 148	syl5 32	. . . . . . 7 $/\$
150	149	rexlimiv 2541	. . . . . 6 $/\$
151	1, 150	sylbi 120	. . . . 5 $/\$
152	151	com13 80	. . . 4 $/\$
153	152	impd 252	. . 3 $/\$ $/\$
154	153	alrimiv 1846	. 2 $/\$ $/\$
155		ineq1 3265	. . . 4
156	155	eleq1d 2206	. . 3
157		ineq2 3266	. . . 4
158	157	eleq1d 2206	. . 3
159	156, 158	cbvral2v 2660	. 2
160		df-3an 964	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 237	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1446	. 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 697 $/\$ w3a 962

wal 1329

wceq 1331

wex 1468

wcel 1480

wne 2306

wral 2414

wrex 2415

cvv 2681

cun 3064

cin 3065

wss 3066

c0 3358

csn 3522

cint 3766 class class class wbr 3924

csuc 4282

com 4499

ccnv 4533

cdm 4534

crn 4535

cima 4537

wfun 5112

wfn 5113

wf 5114

wf1 5115

wfo 5116

wf1o 5117

cfv 5118

cen 6625

cfn 6627

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-sep 4041 ax-nul 4049 ax-pow 4093 ax-pr 4126 ax-un 4350 ax-iinf 4497

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-ral 2419 df-rex 2420 df-v 2683 df-sbc 2905 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-nul 3359 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-int 3767 df-br 3925 df-opab 3985 df-id 4210 df-suc 4288 df-iom 4500 df-xp 4540 df-rel 4541 df-cnv 4542 df-co 4543 df-dm 4544 df-rn 4545 df-res 4546 df-ima 4547 df-iota 5083 df-fun 5120 df-fn 5121 df-f 5122 df-f1 5123 df-fo 5124 df-f1o 5125 df-fv 5126 df-er 6422 df-en 6628 df-fin 6630

This theorem is referenced by: istopfin 12156

W3C validator