fiintim - Intuitionistic Logic Explorer

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

Theorem fiintim 6825

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 6663	. . . . . 6
2		ensym 6683	. . . . . . . 8
3		breq1 3940	. . . . . . . . . . . . . . 15
4	3	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
5	4	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
6	5	albidv 1797	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
7		breq1 3940	. . . . . . . . . . . . . . 15
8	7	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	9	albidv 1797	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11		breq1 3940	. . . . . . . . . . . . . . 15
12	11	anbi2d 460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
13	12	imbi1d 230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	albidv 1797	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		ensym 6683	. . . . . . . . . . . . . . . . . . 19
16		en0 6697	. . . . . . . . . . . . . . . . . . 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 2310	. . . . . . . . . . . . . . . 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 1426	. . . . . . . . . . . . 13 $/\$ $/\$
27	26	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$
28		nfv 1509	. . . . . . . . . . . . . 14 $/\$
29		nfa1 1522	. . . . . . . . . . . . . 14 $/\$ $/\$
30		simpl 108	. . . . . . . . . . . . . . . . 17 $/\$
31		bren 6649	. . . . . . . . . . . . . . . . . . 19
32		ssel 3096	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		f1of 5375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
34		vex 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35	34	sucid 4347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
36		ffvelrn 5561	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
42		ima0 4906	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	41, 42	eqtrdi 2189	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		inteq 3782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45		int0 3793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
46	44, 45	eqtrdi 2189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47	46	ineq1d 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48		ssv 3124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49		sseqin2 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
50	48, 49	mpbi 144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
51	47, 50	eqtrdi 2189	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	51	eleq1d 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	biimprd 157	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	43, 53	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		f1ofun 5377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
57	56	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		elelsuc 4339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	58	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		f1odm 5379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	eleq2d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62	61	ad3antlr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	59, 62	mpbird 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	57, 63	jca 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simpr 109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		funfvima 5657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
67	64, 65, 66	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		ne0i 3374	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	67, 68	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		imassrn 4900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71		dff1o2 5380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
72	71	simp3bi 999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
73	70, 72	sseqtrid 3152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74		sstr2 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
76	75	anim1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
77		f1of1 5374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78		vex 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79		sssucid 4345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80		f1imaen2g 6695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
81	79, 34, 80	mpanr12 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
82	77, 78, 81	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
83	82	ensymd 6685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84	76, 83	jctird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
85		vex 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
86	85	imaex 4902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87		sseq1 3125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88		neeq1 2322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
89	87, 88	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
90		breq2 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91	89, 90	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
92		inteq 3782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	92	eleq1d 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94	91, 93	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
95	86, 94	spcv 2783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
96	84, 95	sylan9 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
97		ineq1 3275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	eleq1d 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		ineq2 3276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	99	eleq1d 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	98, 100	rspc2v 2806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4540	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
112	111	ad3antrrr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
113	55, 110, 112	mpjaodan 788	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	40, 113	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	85, 34	fvex 5449	. . . . . . . . . . . . . . . . . . . . . . . . . 26
116	115	intunsn 3817	. . . . . . . . . . . . . . . . . . . . . . . . 25
117		f1ofn 5376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118		fnsnfv 5488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
119	117, 35, 118	sylancl 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120	119	uneq2d 3235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121		df-suc 4301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122	121	imaeq2i 4887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123		imaundi 4959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	122, 123	eqtr2i 2162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	120, 124	eqtrdi 2189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
126		f1ofo 5382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127		foima 5358	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	126, 127	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	125, 128	eqtrd 2173	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	inteqd 3784	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	116, 130	syl5eqr 2187	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	eleq1d 2209	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ad2antlr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	114, 133	mpbid 146	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp43 370	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
136	135	exlimdv 1792	. . . . . . . . . . . . . . . . . . 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 1590	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	ex 114	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	6, 10, 14, 27, 143	finds2 4523	. . . . . . . . . . 11 $/\$ $/\$
145		sp 1489	. . . . . . . . . . 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 2546	. . . . . 6 $/\$
151	1, 150	sylbi 120	. . . . 5 $/\$
152	151	com13 80	. . . 4 $/\$
153	152	impd 252	. . 3 $/\$ $/\$
154	153	alrimiv 1847	. 2 $/\$ $/\$
155		ineq1 3275	. . . 4
156	155	eleq1d 2209	. . 3
157		ineq2 3276	. . . 4
158	157	eleq1d 2209	. . 3
159	156, 158	cbvral2v 2668	. 2
160		df-3an 965	. . . 4 $/\$ $/\$ $/\$ $/\$
161	160	imbi1i 237	. . 3 $/\$ $/\$ $/\$ $/\$
162	161	albii 1447	. 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 963

wal 1330

wceq 1332

wex 1469

wcel 1481

wne 2309

wral 2417

wrex 2418

cvv 2689

cun 3074

cin 3075

wss 3076

c0 3368

csn 3532

cint 3779 class class class wbr 3937

csuc 4295

com 4512

ccnv 4546

cdm 4547

crn 4548

cima 4550

wfun 5125

wfn 5126

wf 5127

wf1 5128

wfo 5129

wf1o 5130

cfv 5131

cen 6640

cfn 6642

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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-iinf 4510

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-ral 2422 df-rex 2423 df-v 2691 df-sbc 2914 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-br 3938 df-opab 3998 df-id 4223 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-er 6437 df-en 6643 df-fin 6645

This theorem is referenced by: istopfin 12206

W3C validator