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

Theorem fiintim 6862
 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.
StepHypRef Expression
1 isfi 6695 . . . . . 6
2 ensym 6715 . . . . . . . 8
3 breq1 3964 . . . . . . . . . . . . . . 15
43anbi2d 460 . . . . . . . . . . . . . 14
54imbi1d 230 . . . . . . . . . . . . 13
65albidv 1801 . . . . . . . . . . . 12
7 breq1 3964 . . . . . . . . . . . . . . 15
87anbi2d 460 . . . . . . . . . . . . . 14
98imbi1d 230 . . . . . . . . . . . . 13
109albidv 1801 . . . . . . . . . . . 12
11 breq1 3964 . . . . . . . . . . . . . . 15
1211anbi2d 460 . . . . . . . . . . . . . 14
1312imbi1d 230 . . . . . . . . . . . . 13
1413albidv 1801 . . . . . . . . . . . 12
15 ensym 6715 . . . . . . . . . . . . . . . . . . 19
16 en0 6729 . . . . . . . . . . . . . . . . . . 19
1715, 16sylib 121 . . . . . . . . . . . . . . . . . 18
1817anim1i 338 . . . . . . . . . . . . . . . . 17
1918ancoms 266 . . . . . . . . . . . . . . . 16
2019adantll 468 . . . . . . . . . . . . . . 15
21 df-ne 2325 . . . . . . . . . . . . . . . 16
22 pm3.24 683 . . . . . . . . . . . . . . . . 17
2322pm2.21i 636 . . . . . . . . . . . . . . . 16
2421, 23sylan2b 285 . . . . . . . . . . . . . . 15
2520, 24syl 14 . . . . . . . . . . . . . 14
2625ax-gen 1426 . . . . . . . . . . . . 13
2726a1i 9 . . . . . . . . . . . 12
28 nfv 1505 . . . . . . . . . . . . . 14
29 nfa1 1518 . . . . . . . . . . . . . 14
30 simpl 108 . . . . . . . . . . . . . . . . 17
31 bren 6681 . . . . . . . . . . . . . . . . . . 19
32 ssel 3118 . . . . . . . . . . . . . . . . . . . . . . . . . 26
33 f1of 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3534sucid 4372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
36 ffvelrn 5593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3733, 35, 36sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3832, 37impel 278 . . . . . . . . . . . . . . . . . . . . . . . . 25
3938adantr 274 . . . . . . . . . . . . . . . . . . . . . . . 24
4039adantlll 472 . . . . . . . . . . . . . . . . . . . . . . 23
41 imaeq2 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
42 ima0 4938 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4341, 42eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . 26
44 inteq 3806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
45 int0 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4644, 45eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4746ineq1d 3303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48 ssv 3146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49 sseqin2 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5048, 49mpbi 144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5147, 50eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5251eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5352biimprd 157 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25
5554adantl 275 . . . . . . . . . . . . . . . . . . . . . . . 24
56 f1ofun 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5756ad3antlr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58 elelsuc 4364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5958adantl 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60 f1odm 5411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6160eleq2d 2224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6261ad3antlr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6359, 62mpbird 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6457, 63jca 304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
65 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
66 funfvima 5689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26
68 ne0i 3396 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25
70 imassrn 4932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71 dff1o2 5412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
7271simp3bi 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7370, 72sseqtrid 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
74 sstr2 3131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7675anim1d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77 f1of1 5406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79 sssucid 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
80 f1imaen2g 6727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8179, 34, 80mpanr12 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8277, 78, 81sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8382ensymd 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8476, 83jctird 315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
85 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8685imaex 4934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
87 sseq1 3147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
88 neeq1 2337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8987, 88anbi12d 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
90 breq2 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9189, 90anbi12d 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
92 inteq 3806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9392eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9491, 93imbi12d 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9586, 94spcv 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9684, 95sylan9 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97 ineq1 3297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9897eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99 ineq2 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
10099eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
10198, 100rspc2v 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102101ex 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10396, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
104103com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
105104exp5c 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
106105com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
107106imp43 353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108107adantlll 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109108adantr 274 . . . . . . . . . . . . . . . . . . . . . . . . 25
11069, 109mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24
111 0elnn 4572 . . . . . . . . . . . . . . . . . . . . . . . . 25
112111ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . . . . 24
11355, 110, 112mpjaodan 788 . . . . . . . . . . . . . . . . . . . . . . 23
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22
11585, 34fvex 5481 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116115intunsn 3841 . . . . . . . . . . . . . . . . . . . . . . . . 25
117 f1ofn 5408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118 fnsnfv 5520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
119117, 35, 118sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120119uneq2d 3257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121 df-suc 4326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122121imaeq2i 4919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123 imaundi 4991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124122, 123eqtr2i 2176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125120, 124eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
126 f1ofo 5414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127 foima 5390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
129125, 128eqtrd 2187 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130129inteqd 3808 . . . . . . . . . . . . . . . . . . . . . . . . 25
131116, 130syl5eqr 2201 . . . . . . . . . . . . . . . . . . . . . . . 24
132131eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . 23
133132ad2antlr 481 . . . . . . . . . . . . . . . . . . . . . 22
134114, 133mpbid 146 . . . . . . . . . . . . . . . . . . . . 21
135134exp43 370 . . . . . . . . . . . . . . . . . . . 20
136135exlimdv 1796 . . . . . . . . . . . . . . . . . . 19
13731, 136syl5bi 151 . . . . . . . . . . . . . . . . . 18
138137expimpd 361 . . . . . . . . . . . . . . . . 17
13930, 138sylani 404 . . . . . . . . . . . . . . . 16
140139com24 87 . . . . . . . . . . . . . . 15
141140imp 123 . . . . . . . . . . . . . 14
14228, 29, 141alrimd 1587 . . . . . . . . . . . . 13
143142ex 114 . . . . . . . . . . . 12
1446, 10, 14, 27, 143finds2 4554 . . . . . . . . . . 11
145 sp 1488 . . . . . . . . . . 11
146144, 145syl6 33 . . . . . . . . . 10
147146exp4a 364 . . . . . . . . 9
148147com24 87 . . . . . . . 8
1492, 148syl5 32 . . . . . . 7
150149rexlimiv 2565 . . . . . 6
1511, 150sylbi 120 . . . . 5
152151com13 80 . . . 4
153152impd 252 . . 3
154153alrimiv 1851 . 2
155 ineq1 3297 . . . 4
156155eleq1d 2223 . . 3
157 ineq2 3298 . . . 4
158157eleq1d 2223 . . 3
159156, 158cbvral2v 2688 . 2
160 df-3an 965 . . . 4
161160imbi1i 237 . . 3
162161albii 1447 . 2
163154, 159, 1623imtr4i 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 2125   wne 2324  wral 2432  wrex 2433  cvv 2709   cun 3096   cin 3097   wss 3098  c0 3390  csn 3556  cint 3803   class class class wbr 3961   csuc 4320  com 4543  ccnv 4578   cdm 4579   crn 4580  cima 4582   wfun 5157   wfn 5158  wf 5159  wf1 5160  wfo 5161  wf1o 5162  cfv 5163   cen 6672  cfn 6674 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 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-iinf 4541 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-v 2711  df-sbc 2934  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-br 3962  df-opab 4022  df-id 4248  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-er 6469  df-en 6675  df-fin 6677 This theorem is referenced by:  istopfin  12337
 Copyright terms: Public domain W3C validator