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

Theorem fiint 7375
 Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty 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 7123 . . . . . . 7
2 ensym 7148 . . . . . . . . 9
3 breq1 4207 . . . . . . . . . . . . . . . 16
43anbi2d 685 . . . . . . . . . . . . . . 15
54imbi1d 309 . . . . . . . . . . . . . 14
65albidv 1635 . . . . . . . . . . . . 13
7 breq1 4207 . . . . . . . . . . . . . . . 16
87anbi2d 685 . . . . . . . . . . . . . . 15
98imbi1d 309 . . . . . . . . . . . . . 14
109albidv 1635 . . . . . . . . . . . . 13
11 breq1 4207 . . . . . . . . . . . . . . . 16
1211anbi2d 685 . . . . . . . . . . . . . . 15
1312imbi1d 309 . . . . . . . . . . . . . 14
1413albidv 1635 . . . . . . . . . . . . 13
15 ensym 7148 . . . . . . . . . . . . . . . . . . . 20
16 en0 7162 . . . . . . . . . . . . . . . . . . . 20
1715, 16sylib 189 . . . . . . . . . . . . . . . . . . 19
1817anim1i 552 . . . . . . . . . . . . . . . . . 18
1918ancoms 440 . . . . . . . . . . . . . . . . 17
2019adantll 695 . . . . . . . . . . . . . . . 16
21 df-ne 2600 . . . . . . . . . . . . . . . . 17
22 pm3.24 853 . . . . . . . . . . . . . . . . . 18
2322pm2.21i 125 . . . . . . . . . . . . . . . . 17
2421, 23sylan2b 462 . . . . . . . . . . . . . . . 16
2520, 24syl 16 . . . . . . . . . . . . . . 15
2625ax-gen 1555 . . . . . . . . . . . . . 14
2726a1i 11 . . . . . . . . . . . . 13
28 nfv 1629 . . . . . . . . . . . . . . 15
29 nfa1 1806 . . . . . . . . . . . . . . 15
30 bren 7109 . . . . . . . . . . . . . . . . . . 19
31 f1of 5666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
32 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3332sucid 4652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3531, 33, 34sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26
36 ssel 3334 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3735, 36syl5 30 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837imp 419 . . . . . . . . . . . . . . . . . . . . . . . 24
3938adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
40 df-ne 2600 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 imassrn 5208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42 dff1o2 5671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4342simp3bi 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4441, 43syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45 sstr2 3347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4644, 45syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4746anim1d 548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48 f1of1 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50 sssucid 4650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51 f1imaen2g 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5250, 32, 51mpanr12 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5348, 49, 52sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5453ensymd 7150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5547, 54jctird 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
56 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57 imaexg 5209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5856, 57ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59 sseq1 3361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60 neeq1 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6159, 60anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
62 breq2 4208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6361, 62anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64 inteq 4045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6564eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6663, 65imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6758, 66spcv 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6855, 67sylan9 639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 ineq1 3527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7069eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71 ineq2 3528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7271eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7370, 72rspc2v 3050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7473ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7568, 74syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7675com4r 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7776exp5c 600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7877com14 84 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7978imp43 579 . . . . . . . . . . . . . . . . . . . . . . . . 25
8040, 79syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . . 24
81 inteq 4045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82 int0 4056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8381, 82syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8483ineq1d 3533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 ssv 3360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86 sseqin2 3552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8785, 86mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8884, 87syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8988eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089biimprd 215 . . . . . . . . . . . . . . . . . . . . . . . 24
9180, 90pm2.61d2 154 . . . . . . . . . . . . . . . . . . . . . . 23
9239, 91mpd 15 . . . . . . . . . . . . . . . . . . . . . 22
93 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9493intunsn 4081 . . . . . . . . . . . . . . . . . . . . . . . . 25
95 f1ofn 5667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96 fnsnfv 5778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9795, 33, 96sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9897uneq2d 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99 df-suc 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10099imaeq2i 5193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 imaundi 5276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102100, 101eqtr2i 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10398, 102syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
104 f1ofo 5673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105 foima 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
107103, 106eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107inteqd 4047 . . . . . . . . . . . . . . . . . . . . . . . . 25
10994, 108syl5eqr 2481 . . . . . . . . . . . . . . . . . . . . . . . 24
110109eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . 23
111110ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . 22
11292, 111mpbid 202 . . . . . . . . . . . . . . . . . . . . 21
113112exp43 596 . . . . . . . . . . . . . . . . . . . 20
114113exlimdv 1646 . . . . . . . . . . . . . . . . . . 19
11530, 114syl5bi 209 . . . . . . . . . . . . . . . . . 18
116115imp 419 . . . . . . . . . . . . . . . . 17
117116adantlr 696 . . . . . . . . . . . . . . . 16
118117com13 76 . . . . . . . . . . . . . . 15
11928, 29, 118alrimd 1785 . . . . . . . . . . . . . 14
120119a1i 11 . . . . . . . . . . . . 13
1216, 10, 14, 27, 120finds2 4865 . . . . . . . . . . . 12
122 sp 1763 . . . . . . . . . . . 12
123121, 122syl6 31 . . . . . . . . . . 11
124123exp4a 590 . . . . . . . . . 10
125124com24 83 . . . . . . . . 9
1262, 125syl5 30 . . . . . . . 8
127126rexlimiv 2816 . . . . . . 7
1281, 127sylbi 188 . . . . . 6
129128com13 76 . . . . 5
130129imp3a 421 . . . 4
131130alrimiv 1641 . . 3
132 zfpair2 4396 . . . . . 6
133 sseq1 3361 . . . . . . . . 9
134 neeq1 2606 . . . . . . . . 9
135133, 134anbi12d 692 . . . . . . . 8
136 eleq1 2495 . . . . . . . 8
137135, 136anbi12d 692 . . . . . . 7
138 inteq 4045 . . . . . . . 8
139138eleq1d 2501 . . . . . . 7
140137, 139imbi12d 312 . . . . . 6
141132, 140spcv 3034 . . . . 5
142 vex 2951 . . . . . . 7
143 vex 2951 . . . . . . 7
144142, 143prss 3944 . . . . . 6
145142prnz 3915 . . . . . . 7
146145biantru 492 . . . . . 6
147 prfi 7373 . . . . . . 7
148147biantru 492 . . . . . 6
149144, 146, 1483bitrri 264 . . . . 5
150142, 143intpr 4075 . . . . . 6
151150eleq1i 2498 . . . . 5
152141, 149, 1513imtr3g 261 . . . 4
153152ralrimivv 2789 . . 3
154131, 153impbii 181 . 2
155 ineq1 3527 . . . 4
156155eleq1d 2501 . . 3
157 ineq2 3528 . . . 4
158157eleq1d 2501 . . 3
159156, 158cbvral2v 2932 . 2
160 df-3an 938 . . . 4
161160imbi1i 316 . . 3
162161albii 1575 . 2
163154, 159, 1623bitr4i 269 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   w3a 936  wal 1549  wex 1550   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698  cvv 2948   cun 3310   cin 3311   wss 3312  c0 3620  csn 3806  cpr 3807  cint 4042   class class class wbr 4204   csuc 4575  com 4837  ccnv 4869   crn 4871  cima 4873   wfun 5440   wfn 5441  wf 5442  wf1 5443  wfo 5444  wf1o 5445  cfv 5446   cen 7098  cfn 7101 This theorem is referenced by:  dffi2  7420  istop2g  16961  istps4OLD  16980  neificl  26450 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-er 6897  df-en 7102  df-fin 7105
 Copyright terms: Public domain W3C validator