Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fiint Structured version   Visualization version   Unicode version

Theorem fiint 7848
 Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of is in ." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.)
Assertion
Ref Expression
fiint
Distinct variable group:   ,,

Proof of Theorem fiint
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 7593 . . . . . . 7
2 ensym 7618 . . . . . . . . 9
3 breq1 4405 . . . . . . . . . . . . . . . 16
43anbi2d 710 . . . . . . . . . . . . . . 15
54imbi1d 319 . . . . . . . . . . . . . 14
65albidv 1767 . . . . . . . . . . . . 13
7 breq1 4405 . . . . . . . . . . . . . . . 16
87anbi2d 710 . . . . . . . . . . . . . . 15
98imbi1d 319 . . . . . . . . . . . . . 14
109albidv 1767 . . . . . . . . . . . . 13
11 breq1 4405 . . . . . . . . . . . . . . . 16
1211anbi2d 710 . . . . . . . . . . . . . . 15
1312imbi1d 319 . . . . . . . . . . . . . 14
1413albidv 1767 . . . . . . . . . . . . 13
15 ensym 7618 . . . . . . . . . . . . . . . . . . . 20
16 en0 7632 . . . . . . . . . . . . . . . . . . . 20
1715, 16sylib 200 . . . . . . . . . . . . . . . . . . 19
1817anim1i 572 . . . . . . . . . . . . . . . . . 18
1918ancoms 455 . . . . . . . . . . . . . . . . 17
2019adantll 720 . . . . . . . . . . . . . . . 16
21 df-ne 2624 . . . . . . . . . . . . . . . . 17
22 pm3.24 893 . . . . . . . . . . . . . . . . . 18
2322pm2.21i 135 . . . . . . . . . . . . . . . . 17
2421, 23sylan2b 478 . . . . . . . . . . . . . . . 16
2520, 24syl 17 . . . . . . . . . . . . . . 15
2625ax-gen 1669 . . . . . . . . . . . . . 14
2726a1i 11 . . . . . . . . . . . . 13
28 nfv 1761 . . . . . . . . . . . . . . 15
29 nfa1 1979 . . . . . . . . . . . . . . 15
30 bren 7578 . . . . . . . . . . . . . . . . . . 19
31 f1of 5814 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
32 vex 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3332sucid 5502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34 ffvelrn 6020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3531, 33, 34sylancl 668 . . . . . . . . . . . . . . . . . . . . . . . . . 26
36 ssel 3426 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3735, 36syl5 33 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837imp 431 . . . . . . . . . . . . . . . . . . . . . . . 24
3938adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23
40 df-ne 2624 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 imassrn 5179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42 dff1o2 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4342simp3bi 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4441, 43syl5sseq 3480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45 sstr2 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4746anim1d 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48 f1of1 5813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49 vex 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50 sssucid 5500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51 f1imaen2g 7630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5250, 32, 51mpanr12 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5348, 49, 52sylancl 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5453ensymd 7620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5547, 54jctird 547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
56 vex 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57 imaexg 6730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59 sseq1 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60 neeq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6159, 60anbi12d 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
62 breq2 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6361, 62anbi12d 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64 inteq 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6564eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6663, 65imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6758, 66spcv 3140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6855, 67sylan9 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 ineq1 3627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7069eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71 ineq2 3628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7271eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7370, 72rspc2v 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7473ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7568, 74syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7675com4r 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7776exp5c 621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7877com14 91 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7978imp43 600 . . . . . . . . . . . . . . . . . . . . . . . . 25
8040, 79syl5bir 222 . . . . . . . . . . . . . . . . . . . . . . . 24
81 inteq 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82 int0 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8381, 82syl6eq 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8483ineq1d 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 ssv 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86 sseqin2 3651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8785, 86mpbi 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8884, 87syl6eq 2501 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8988eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089biimprd 227 . . . . . . . . . . . . . . . . . . . . . . . 24
9180, 90pm2.61d2 164 . . . . . . . . . . . . . . . . . . . . . . 23
9239, 91mpd 15 . . . . . . . . . . . . . . . . . . . . . 22
93 fvex 5875 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9493intunsn 4274 . . . . . . . . . . . . . . . . . . . . . . . . 25
95 f1ofn 5815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96 fnsnfv 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9795, 33, 96sylancl 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9897uneq2d 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99 df-suc 5429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10099imaeq2i 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 imaundi 5248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102100, 101eqtr2i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10398, 102syl6eq 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
104 f1ofo 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105 foima 5798 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
107103, 106eqtrd 2485 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107inteqd 4239 . . . . . . . . . . . . . . . . . . . . . . . . 25
10994, 108syl5eqr 2499 . . . . . . . . . . . . . . . . . . . . . . . 24
110109eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . . 23
111110ad2antlr 733 . . . . . . . . . . . . . . . . . . . . . 22
11292, 111mpbid 214 . . . . . . . . . . . . . . . . . . . . 21
113112exp43 617 . . . . . . . . . . . . . . . . . . . 20
114113exlimdv 1779 . . . . . . . . . . . . . . . . . . 19
11530, 114syl5bi 221 . . . . . . . . . . . . . . . . . 18
116115imp 431 . . . . . . . . . . . . . . . . 17
117116adantlr 721 . . . . . . . . . . . . . . . 16
118117com13 83 . . . . . . . . . . . . . . 15
11928, 29, 118alrimd 1959 . . . . . . . . . . . . . 14
120119a1i 11 . . . . . . . . . . . . 13
1216, 10, 14, 27, 120finds2 6721 . . . . . . . . . . . 12
122 sp 1937 . . . . . . . . . . . 12
123121, 122syl6 34 . . . . . . . . . . 11
124123exp4a 611 . . . . . . . . . 10
125124com24 90 . . . . . . . . 9
1262, 125syl5 33 . . . . . . . 8
127126rexlimiv 2873 . . . . . . 7
1281, 127sylbi 199 . . . . . 6
129128com13 83 . . . . 5
130129impd 433 . . . 4
131130alrimiv 1773 . . 3
132 zfpair2 4640 . . . . . 6
133 sseq1 3453 . . . . . . . . 9
134 neeq1 2686 . . . . . . . . 9
135133, 134anbi12d 717 . . . . . . . 8
136 eleq1 2517 . . . . . . . 8
137135, 136anbi12d 717 . . . . . . 7
138 inteq 4237 . . . . . . . 8
139138eleq1d 2513 . . . . . . 7
140137, 139imbi12d 322 . . . . . 6
141132, 140spcv 3140 . . . . 5
142 vex 3048 . . . . . . 7
143 vex 3048 . . . . . . 7
144142, 143prss 4126 . . . . . 6
145142prnz 4091 . . . . . . 7
146145biantru 508 . . . . . 6
147 prfi 7846 . . . . . . 7
148147biantru 508 . . . . . 6
149144, 146, 1483bitrri 276 . . . . 5
150142, 143intpr 4268 . . . . . 6
151150eleq1i 2520 . . . . 5
152141, 149, 1513imtr3g 273 . . . 4
153152ralrimivv 2808 . . 3
154131, 153impbii 191 . 2
155 ineq1 3627 . . . 4
156155eleq1d 2513 . . 3
157 ineq2 3628 . . . 4
158157eleq1d 2513 . . 3
159156, 158cbvral2v 3027 . 2
160 df-3an 987 . . . 4
161160imbi1i 327 . . 3
162161albii 1691 . 2
163154, 159, 1623bitr4i 281 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   w3a 985  wal 1442   wceq 1444  wex 1663   wcel 1887   wne 2622  wral 2737  wrex 2738  cvv 3045   cun 3402   cin 3403   wss 3404  c0 3731  csn 3968  cpr 3970  cint 4234   class class class wbr 4402  ccnv 4833   crn 4835  cima 4837   csuc 5425   wfun 5576   wfn 5577  wf 5578  wf1 5579  wfo 5580  wf1o 5581  cfv 5582  com 6692   cen 7566  cfn 7569 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-en 7570  df-fin 7573 This theorem is referenced by:  dffi2  7937  istop2g  19926  neificl  32082
 Copyright terms: Public domain W3C validator