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

Theorem fiint 7817
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 7559 . . . . . . 7
2 ensym 7584 . . . . . . . . 9
3 breq1 4455 . . . . . . . . . . . . . . . 16
43anbi2d 703 . . . . . . . . . . . . . . 15
54imbi1d 317 . . . . . . . . . . . . . 14
65albidv 1713 . . . . . . . . . . . . 13
7 breq1 4455 . . . . . . . . . . . . . . . 16
87anbi2d 703 . . . . . . . . . . . . . . 15
98imbi1d 317 . . . . . . . . . . . . . 14
109albidv 1713 . . . . . . . . . . . . 13
11 breq1 4455 . . . . . . . . . . . . . . . 16
1211anbi2d 703 . . . . . . . . . . . . . . 15
1312imbi1d 317 . . . . . . . . . . . . . 14
1413albidv 1713 . . . . . . . . . . . . 13
15 ensym 7584 . . . . . . . . . . . . . . . . . . . 20
16 en0 7598 . . . . . . . . . . . . . . . . . . . 20
1715, 16sylib 196 . . . . . . . . . . . . . . . . . . 19
1817anim1i 568 . . . . . . . . . . . . . . . . . 18
1918ancoms 453 . . . . . . . . . . . . . . . . 17
2019adantll 713 . . . . . . . . . . . . . . . 16
21 df-ne 2654 . . . . . . . . . . . . . . . . 17
22 pm3.24 882 . . . . . . . . . . . . . . . . . 18
2322pm2.21i 131 . . . . . . . . . . . . . . . . 17
2421, 23sylan2b 475 . . . . . . . . . . . . . . . 16
2520, 24syl 16 . . . . . . . . . . . . . . 15
2625ax-gen 1618 . . . . . . . . . . . . . 14
2726a1i 11 . . . . . . . . . . . . 13
28 nfv 1707 . . . . . . . . . . . . . . 15
29 nfa1 1897 . . . . . . . . . . . . . . 15
30 bren 7545 . . . . . . . . . . . . . . . . . . 19
31 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
32 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3332sucid 4962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3531, 33, 34sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . 26
36 ssel 3497 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3735, 36syl5 32 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
3938adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
40 df-ne 2654 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 imassrn 5353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
42 dff1o2 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4342simp3bi 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4441, 43syl5sseq 3551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
45 sstr2 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4644, 45syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4746anim1d 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48 f1of1 5820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
50 sssucid 4960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51 f1imaen2g 7596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5250, 32, 51mpanr12 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5348, 49, 52sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5453ensymd 7586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5547, 54jctird 544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
56 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57 imaexg 6737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59 sseq1 3524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
60 neeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6159, 60anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
62 breq2 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6361, 62anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64 inteq 4289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6564eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6663, 65imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6758, 66spcv 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6855, 67sylan9 657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 ineq1 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7069eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71 ineq2 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7271eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7370, 72rspc2v 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7473ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7568, 74syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7675com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7776exp5c 616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7877com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7978imp43 595 . . . . . . . . . . . . . . . . . . . . . . . . 25
8040, 79syl5bir 218 . . . . . . . . . . . . . . . . . . . . . . . 24
81 inteq 4289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82 int0 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8381, 82syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8483ineq1d 3698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 ssv 3523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86 sseqin2 3716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8785, 86mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8884, 87syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8988eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . 24
9180, 90pm2.61d2 160 . . . . . . . . . . . . . . . . . . . . . . 23
9239, 91mpd 15 . . . . . . . . . . . . . . . . . . . . . 22
93 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9493intunsn 4326 . . . . . . . . . . . . . . . . . . . . . . . . 25
95 f1ofn 5822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96 fnsnfv 5933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9795, 33, 96sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9897uneq2d 3657 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99 df-suc 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10099imaeq2i 5340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 imaundi 5423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102100, 101eqtr2i 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10398, 102syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
104 f1ofo 5828 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105 foima 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
107103, 106eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107inteqd 4291 . . . . . . . . . . . . . . . . . . . . . . . . 25
10994, 108syl5eqr 2512 . . . . . . . . . . . . . . . . . . . . . . . 24
110109eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . 23
111110ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22
11292, 111mpbid 210 . . . . . . . . . . . . . . . . . . . . 21
113112exp43 612 . . . . . . . . . . . . . . . . . . . 20
114113exlimdv 1724 . . . . . . . . . . . . . . . . . . 19
11530, 114syl5bi 217 . . . . . . . . . . . . . . . . . 18
116115imp 429 . . . . . . . . . . . . . . . . 17
117116adantlr 714 . . . . . . . . . . . . . . . 16
118117com13 80 . . . . . . . . . . . . . . 15
11928, 29, 118alrimd 1881 . . . . . . . . . . . . . 14
120119a1i 11 . . . . . . . . . . . . 13
1216, 10, 14, 27, 120finds2 6728 . . . . . . . . . . . 12
122 sp 1859 . . . . . . . . . . . 12
123121, 122syl6 33 . . . . . . . . . . 11
124123exp4a 606 . . . . . . . . . 10
125124com24 87 . . . . . . . . 9
1262, 125syl5 32 . . . . . . . 8
127126rexlimiv 2943 . . . . . . 7
1281, 127sylbi 195 . . . . . 6
129128com13 80 . . . . 5
130129impd 431 . . . 4
131130alrimiv 1719 . . 3
132 zfpair2 4692 . . . . . 6
133 sseq1 3524 . . . . . . . . 9
134 neeq1 2738 . . . . . . . . 9
135133, 134anbi12d 710 . . . . . . . 8
136 eleq1 2529 . . . . . . . 8
137135, 136anbi12d 710 . . . . . . 7
138 inteq 4289 . . . . . . . 8
139138eleq1d 2526 . . . . . . 7
140137, 139imbi12d 320 . . . . . 6
141132, 140spcv 3200 . . . . 5
142 vex 3112 . . . . . . 7
143 vex 3112 . . . . . . 7
144142, 143prss 4184 . . . . . 6
145142prnz 4149 . . . . . . 7
146145biantru 505 . . . . . 6
147 prfi 7815 . . . . . . 7
148147biantru 505 . . . . . 6
149144, 146, 1483bitrri 272 . . . . 5
150142, 143intpr 4320 . . . . . 6
151150eleq1i 2534 . . . . 5
152141, 149, 1513imtr3g 269 . . . 4
153152ralrimivv 2877 . . 3
154131, 153impbii 188 . 2
155 ineq1 3692 . . . 4
156155eleq1d 2526 . . 3
157 ineq2 3693 . . . 4
158157eleq1d 2526 . . 3
159156, 158cbvral2v 3092 . 2
160 df-3an 975 . . . 4
161160imbi1i 325 . . 3
162161albii 1640 . 2
163154, 159, 1623bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808   cvv 3109  u.cun 3473  i^icin 3474  C_wss 3475   c0 3784  {csn 4029  {cpr 4031  |^|cint 4286   class class class wbr 4452  succsuc 4885  `'ccnv 5003  rancrn 5005  "cima 5007  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592  `cfv 5593   com 6700   cen 7533   cfn 7536
This theorem is referenced by:  dffi2  7903  istop2g  19405  istps4OLD  19424  neificl  30246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-en 7537  df-fin 7540
  Copyright terms: Public domain W3C validator