Metamath Proof Explorer


Theorem fiint

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 A is in A ". 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)

Ref Expression
Assertion fiint xAyAxyAxxAxxFinxA

Proof

Step Hyp Ref Expression
1 isfi xFinyωxy
2 ensym xyyx
3 breq1 y=yxx
4 3 anbi2d y=xAxyxxAxx
5 4 imbi1d y=xAxyxxAxAxxxA
6 5 albidv y=xxAxyxxAxxAxxxA
7 breq1 y=vyxvx
8 7 anbi2d y=vxAxyxxAxvx
9 8 imbi1d y=vxAxyxxAxAxvxxA
10 9 albidv y=vxxAxyxxAxxAxvxxA
11 breq1 y=sucvyxsucvx
12 11 anbi2d y=sucvxAxyxxAxsucvx
13 12 imbi1d y=sucvxAxyxxAxAxsucvxxA
14 13 albidv y=sucvxxAxyxxAxxAxsucvxxA
15 ensym xx
16 en0 xx=
17 15 16 sylib xx=
18 17 anim1i xxx=x
19 18 ancoms xxx=x
20 19 adantll xAxxx=x
21 df-ne x¬x=
22 pm3.24 ¬x=¬x=
23 22 pm2.21i x=¬x=xA
24 21 23 sylan2b x=xxA
25 20 24 syl xAxxxA
26 25 ax-gen xxAxxxA
27 26 a1i zAwAzwAxxAxxxA
28 nfv xzAwAzwA
29 nfa1 xxxAxvxxA
30 bren sucvxff:sucv1-1 ontox
31 ssel xAfvxfvA
32 f1of f:sucv1-1 ontoxf:sucvx
33 vex vV
34 33 sucid vsucv
35 ffvelrn f:sucvxvsucvfvx
36 32 34 35 sylancl f:sucv1-1 ontoxfvx
37 31 36 impel xAf:sucv1-1 ontoxfvA
38 37 adantr xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvA
39 df-ne fv¬fv=
40 imassrn fvranf
41 dff1o2 f:sucv1-1 ontoxfFnsucvFunf-1ranf=x
42 41 simp3bi f:sucv1-1 ontoxranf=x
43 40 42 sseqtrid f:sucv1-1 ontoxfvx
44 sstr2 fvxxAfvA
45 43 44 syl f:sucv1-1 ontoxxAfvA
46 45 anim1d f:sucv1-1 ontoxxAfvfvAfv
47 f1of1 f:sucv1-1 ontoxf:sucv1-1x
48 vex xV
49 sssucid vsucv
50 f1imaen2g f:sucv1-1xxVvsucvvVfvv
51 49 33 50 mpanr12 f:sucv1-1xxVfvv
52 47 48 51 sylancl f:sucv1-1 ontoxfvv
53 52 ensymd f:sucv1-1 ontoxvfv
54 46 53 jctird f:sucv1-1 ontoxxAfvfvAfvvfv
55 vex fV
56 55 imaex fvV
57 sseq1 x=fvxAfvA
58 neeq1 x=fvxfv
59 57 58 anbi12d x=fvxAxfvAfv
60 breq2 x=fvvxvfv
61 59 60 anbi12d x=fvxAxvxfvAfvvfv
62 inteq x=fvx=fv
63 62 eleq1d x=fvxAfvA
64 61 63 imbi12d x=fvxAxvxxAfvAfvvfvfvA
65 56 64 spcv xxAxvxxAfvAfvvfvfvA
66 54 65 sylan9 f:sucv1-1 ontoxxxAxvxxAxAfvfvA
67 ineq1 z=fvzw=fvw
68 67 eleq1d z=fvzwAfvwA
69 ineq2 w=fvfvw=fvfv
70 69 eleq1d w=fvfvwAfvfvA
71 68 70 rspc2v fvAfvAzAwAzwAfvfvA
72 71 ex fvAfvAzAwAzwAfvfvA
73 66 72 syl6 f:sucv1-1 ontoxxxAxvxxAxAfvfvAzAwAzwAfvfvA
74 73 com4r zAwAzwAf:sucv1-1 ontoxxxAxvxxAxAfvfvAfvfvA
75 74 exp5c zAwAzwAf:sucv1-1 ontoxxxAxvxxAxAfvfvAfvfvA
76 75 com14 xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvfvAfvfvA
77 76 imp43 xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvfvAfvfvA
78 39 77 syl5bir xAf:sucv1-1 ontoxxxAxvxxAzAwAzwA¬fv=fvAfvfvA
79 inteq fv=fv=
80 int0 =V
81 79 80 eqtrdi fv=fv=V
82 81 ineq1d fv=fvfv=Vfv
83 ssv fvV
84 sseqin2 fvVVfv=fv
85 83 84 mpbi Vfv=fv
86 82 85 eqtrdi fv=fvfv=fv
87 86 eleq1d fv=fvfvAfvA
88 87 biimprd fv=fvAfvfvA
89 78 88 pm2.61d2 xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvAfvfvA
90 38 89 mpd xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvfvA
91 fvex fvV
92 91 intunsn fvfv=fvfv
93 f1ofn f:sucv1-1 ontoxfFnsucv
94 fnsnfv fFnsucvvsucvfv=fv
95 93 34 94 sylancl f:sucv1-1 ontoxfv=fv
96 95 uneq2d f:sucv1-1 ontoxfvfv=fvfv
97 df-suc sucv=vv
98 97 imaeq2i fsucv=fvv
99 imaundi fvv=fvfv
100 98 99 eqtr2i fvfv=fsucv
101 96 100 eqtrdi f:sucv1-1 ontoxfvfv=fsucv
102 f1ofo f:sucv1-1 ontoxf:sucvontox
103 foima f:sucvontoxfsucv=x
104 102 103 syl f:sucv1-1 ontoxfsucv=x
105 101 104 eqtrd f:sucv1-1 ontoxfvfv=x
106 105 inteqd f:sucv1-1 ontoxfvfv=x
107 92 106 eqtr3id f:sucv1-1 ontoxfvfv=x
108 107 eleq1d f:sucv1-1 ontoxfvfvAxA
109 108 ad2antlr xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAfvfvAxA
110 90 109 mpbid xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAxA
111 110 exp43 xAf:sucv1-1 ontoxxxAxvxxAzAwAzwAxA
112 111 exlimdv xAff:sucv1-1 ontoxxxAxvxxAzAwAzwAxA
113 30 112 syl5bi xAsucvxxxAxvxxAzAwAzwAxA
114 113 imp xAsucvxxxAxvxxAzAwAzwAxA
115 114 adantlr xAxsucvxxxAxvxxAzAwAzwAxA
116 115 com13 zAwAzwAxxAxvxxAxAxsucvxxA
117 28 29 116 alrimd zAwAzwAxxAxvxxAxxAxsucvxxA
118 117 a1i vωzAwAzwAxxAxvxxAxxAxsucvxxA
119 6 10 14 27 118 finds2 yωzAwAzwAxxAxyxxA
120 sp xxAxyxxAxAxyxxA
121 119 120 syl6 yωzAwAzwAxAxyxxA
122 121 exp4a yωzAwAzwAxAxyxxA
123 122 com24 yωyxxAxzAwAzwAxA
124 2 123 syl5 yωxyxAxzAwAzwAxA
125 124 rexlimiv yωxyxAxzAwAzwAxA
126 1 125 sylbi xFinxAxzAwAzwAxA
127 126 com13 zAwAzwAxAxxFinxA
128 127 impd zAwAzwAxAxxFinxA
129 128 alrimiv zAwAzwAxxAxxFinxA
130 zfpair2 zwV
131 sseq1 x=zwxAzwA
132 neeq1 x=zwxzw
133 131 132 anbi12d x=zwxAxzwAzw
134 eleq1 x=zwxFinzwFin
135 133 134 anbi12d x=zwxAxxFinzwAzwzwFin
136 inteq x=zwx=zw
137 136 eleq1d x=zwxAzwA
138 135 137 imbi12d x=zwxAxxFinxAzwAzwzwFinzwA
139 130 138 spcv xxAxxFinxAzwAzwzwFinzwA
140 vex zV
141 vex wV
142 140 141 prss zAwAzwA
143 140 prnz zw
144 143 biantru zwAzwAzw
145 prfi zwFin
146 145 biantru zwAzwzwAzwzwFin
147 142 144 146 3bitrri zwAzwzwFinzAwA
148 140 141 intpr zw=zw
149 148 eleq1i zwAzwA
150 139 147 149 3imtr3g xxAxxFinxAzAwAzwA
151 150 ralrimivv xxAxxFinxAzAwAzwA
152 129 151 impbii zAwAzwAxxAxxFinxA
153 ineq1 x=zxy=zy
154 153 eleq1d x=zxyAzyA
155 ineq2 y=wzy=zw
156 155 eleq1d y=wzyAzwA
157 154 156 cbvral2vw xAyAxyAzAwAzwA
158 df-3an xAxxFinxAxxFin
159 158 imbi1i xAxxFinxAxAxxFinxA
160 159 albii xxAxxFinxAxxAxxFinxA
161 152 157 160 3bitr4i xAyAxyAxxAxxFinxA