Metamath Proof Explorer


Theorem disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjinfi.b φxABV
disjinfi.d φDisjxAB
disjinfi.c φCFin
Assertion disjinfi φxA|BCFin

Proof

Step Hyp Ref Expression
1 disjinfi.b φxABV
2 disjinfi.d φDisjxAB
3 disjinfi.c φCFin
4 inss2 ranxABCC
5 ssfi CFinranxABCCranxABCFin
6 3 4 5 sylancl φranxABCFin
7 4 a1i φranxABCC
8 3 7 ssexd φranxABCV
9 elinel1 yranxABCyranxAB
10 eluni2 yranxABwranxAByw
11 10 biimpi yranxABwranxAByw
12 eqid xAB=xAB
13 12 elrnmpt wVwranxABxAw=B
14 13 elv wranxABxAw=B
15 14 biimpi wranxABxAw=B
16 15 adantr wranxABywxAw=B
17 nfmpt1 _xxAB
18 17 nfrn _xranxAB
19 18 nfcri xwranxAB
20 nfv xyw
21 19 20 nfan xwranxAByw
22 simpl yww=Byw
23 simpr yww=Bw=B
24 22 23 eleqtrd yww=ByB
25 24 ex yww=ByB
26 25 a1d ywxAw=ByB
27 26 adantl wranxABywxAw=ByB
28 21 27 reximdai wranxABywxAw=BxAyB
29 16 28 mpd wranxABywxAyB
30 29 ex wranxABywxAyB
31 30 a1i yranxABwranxABywxAyB
32 31 rexlimdv yranxABwranxABywxAyB
33 11 32 mpd yranxABxAyB
34 9 33 syl yranxABCxAyB
35 34 adantl φyranxABCxAyB
36 nfv xφ
37 18 nfuni _xranxAB
38 nfcv _xC
39 37 38 nfin _xranxABC
40 39 nfcri xyranxABC
41 36 40 nfan xφyranxABC
42 nfre1 xxAyBC
43 elinel2 yranxABCyC
44 simp2 yCxAyBxA
45 simpr yCyByB
46 simpl yCyByC
47 45 46 elind yCyByBC
48 rspe xAyBCxAyBC
49 44 47 48 3imp3i2an yCxAyBxAyBC
50 49 3exp yCxAyBxAyBC
51 43 50 syl yranxABCxAyBxAyBC
52 51 adantl φyranxABCxAyBxAyBC
53 41 42 52 rexlimd φyranxABCxAyBxAyBC
54 35 53 mpd φyranxABCxAyBC
55 disjors DisjxABzAwAz=wz/xBw/xB=
56 2 55 sylib φzAwAz=wz/xBw/xB=
57 nfv zwAx=wBw/xB=
58 nfcv _xA
59 nfv xz=w
60 nfcsb1v _xz/xB
61 nfcv _xw
62 61 nfcsb1 _xw/xB
63 60 62 nfin _xz/xBw/xB
64 63 nfeq1 xz/xBw/xB=
65 59 64 nfor xz=wz/xBw/xB=
66 58 65 nfralw xwAz=wz/xBw/xB=
67 equequ1 x=zx=wz=w
68 csbeq1a x=zB=z/xB
69 68 ineq1d x=zBw/xB=z/xBw/xB
70 69 eqeq1d x=zBw/xB=z/xBw/xB=
71 67 70 orbi12d x=zx=wBw/xB=z=wz/xBw/xB=
72 71 ralbidv x=zwAx=wBw/xB=wAz=wz/xBw/xB=
73 57 66 72 cbvralw xAwAx=wBw/xB=zAwAz=wz/xBw/xB=
74 56 73 sylibr φxAwAx=wBw/xB=
75 74 r19.21bi φxAwAx=wBw/xB=
76 rspa wAx=wBw/xB=wAx=wBw/xB=
77 76 orcomd wAx=wBw/xB=wABw/xB=x=w
78 75 77 sylan φxAwABw/xB=x=w
79 elinel1 yBCyB
80 sbsbc wxyBC[˙w/x]˙yBC
81 sbcel2 [˙w/x]˙yBCyw/xBC
82 csbin w/xBC=w/xBw/xC
83 82 eleq2i yw/xBCyw/xBw/xC
84 80 81 83 3bitri wxyBCyw/xBw/xC
85 elinel1 yw/xBw/xCyw/xB
86 84 85 sylbi wxyBCyw/xB
87 inelcm yByw/xBBw/xB
88 87 neneqd yByw/xB¬Bw/xB=
89 79 86 88 syl2an yBCwxyBC¬Bw/xB=
90 pm2.53 Bw/xB=x=w¬Bw/xB=x=w
91 78 89 90 syl2im φxAwAyBCwxyBCx=w
92 91 ralrimiva φxAwAyBCwxyBCx=w
93 92 ralrimiva φxAwAyBCwxyBCx=w
94 93 adantr φyranxABCxAwAyBCwxyBCx=w
95 reu2 ∃!xAyBCxAyBCxAwAyBCwxyBCx=w
96 54 94 95 sylanbrc φyranxABC∃!xAyBC
97 riotacl2 ∃!xAyBCιxA|yBCxA|yBC
98 nfriota1 _xιxA|yBC
99 98 nfcsb1 _xιxA|yBC/xB
100 99 38 nfin _xιxA|yBC/xBC
101 100 nfcri xyιxA|yBC/xBC
102 csbeq1a x=ιxA|yBCB=ιxA|yBC/xB
103 102 ineq1d x=ιxA|yBCBC=ιxA|yBC/xBC
104 103 eleq2d x=ιxA|yBCyBCyιxA|yBC/xBC
105 98 58 101 104 elrabf ιxA|yBCxA|yBCιxA|yBCAyιxA|yBC/xBC
106 105 simplbi ιxA|yBCxA|yBCιxA|yBCA
107 105 simprbi ιxA|yBCxA|yBCyιxA|yBC/xBC
108 107 ne0d ιxA|yBCxA|yBCιxA|yBC/xBC
109 nfcv _x
110 100 109 nfne xιxA|yBC/xBC
111 103 neeq1d x=ιxA|yBCBCιxA|yBC/xBC
112 98 58 110 111 elrabf ιxA|yBCxA|BCιxA|yBCAιxA|yBC/xBC
113 106 108 112 sylanbrc ιxA|yBCxA|yBCιxA|yBCxA|BC
114 96 97 113 3syl φyranxABCιxA|yBCxA|BC
115 114 ralrimiva φyranxABCιxA|yBCxA|BC
116 62 38 nfin _xw/xBC
117 116 109 nfne xw/xBC
118 csbeq1a x=wB=w/xB
119 118 ineq1d x=wBC=w/xBC
120 119 neeq1d x=wBCw/xBC
121 61 58 117 120 elrabf wxA|BCwAw/xBC
122 121 simprbi wxA|BCw/xBC
123 n0 w/xBCyyw/xBC
124 122 123 sylib wxA|BCyyw/xBC
125 124 adantl φwxA|BCyyw/xBC
126 121 simplbi wxA|BCwA
127 elinel1 yw/xBCyw/xB
128 127 adantl φwAyw/xBCyw/xB
129 simplr φwAyw/xBCwA
130 nfv xφwA
131 62 nfel1 xw/xBV
132 130 131 nfim xφwAw/xBV
133 eleq1w x=wxAwA
134 133 anbi2d x=wφxAφwA
135 118 eleq1d x=wBVw/xBV
136 134 135 imbi12d x=wφxABVφwAw/xBV
137 132 136 1 chvarfv φwAw/xBV
138 137 adantr φwAyw/xBCw/xBV
139 eqid wAw/xB=wAw/xB
140 139 elrnmpt1 wAw/xBVw/xBranwAw/xB
141 129 138 140 syl2anc φwAyw/xBCw/xBranwAw/xB
142 nfcv _wB
143 118 equcoms w=xB=w/xB
144 143 eqcomd w=xw/xB=B
145 62 142 144 cbvmpt wAw/xB=xAB
146 145 rneqi ranwAw/xB=ranxAB
147 141 146 eleqtrdi φwAyw/xBCw/xBranxAB
148 elunii yw/xBw/xBranxAByranxAB
149 128 147 148 syl2anc φwAyw/xBCyranxAB
150 elinel2 yw/xBCyC
151 150 adantl φwAyw/xBCyC
152 149 151 elind φwAyw/xBCyranxABC
153 nfv wyBC
154 116 nfcri xyw/xBC
155 119 eleq2d x=wyBCyw/xBC
156 153 154 155 cbvriotaw ιxA|yBC=ιwA|yw/xBC
157 simpr φwAyw/xBCyw/xBC
158 rspe wAyw/xBCwAyw/xBC
159 158 adantll φwAyw/xBCwAyw/xBC
160 simpll φwAyw/xBCφ
161 sbequ w=zwxyBCzxyBC
162 sbsbc zxyBC[˙z/x]˙yBC
163 162 a1i w=zzxyBC[˙z/x]˙yBC
164 sbcel2 [˙z/x]˙yBCyz/xBC
165 csbin z/xBC=z/xBz/xC
166 csbconstg zVz/xC=C
167 166 elv z/xC=C
168 167 ineq2i z/xBz/xC=z/xBC
169 165 168 eqtri z/xBC=z/xBC
170 169 eleq2i yz/xBCyz/xBC
171 164 170 bitri [˙z/x]˙yBCyz/xBC
172 171 a1i w=z[˙z/x]˙yBCyz/xBC
173 161 163 172 3bitrd w=zwxyBCyz/xBC
174 173 anbi2d w=zyBCwxyBCyBCyz/xBC
175 equequ2 w=zx=wx=z
176 174 175 imbi12d w=zyBCwxyBCx=wyBCyz/xBCx=z
177 176 cbvralvw wAyBCwxyBCx=wzAyBCyz/xBCx=z
178 177 ralbii xAwAyBCwxyBCx=wxAzAyBCyz/xBCx=z
179 nfv wzAyBCyz/xBCx=z
180 60 38 nfin _xz/xBC
181 180 nfcri xyz/xBC
182 154 181 nfan xyw/xBCyz/xBC
183 nfv xw=z
184 182 183 nfim xyw/xBCyz/xBCw=z
185 58 184 nfralw xzAyw/xBCyz/xBCw=z
186 155 anbi1d x=wyBCyz/xBCyw/xBCyz/xBC
187 equequ1 x=wx=zw=z
188 186 187 imbi12d x=wyBCyz/xBCx=zyw/xBCyz/xBCw=z
189 188 ralbidv x=wzAyBCyz/xBCx=zzAyw/xBCyz/xBCw=z
190 179 185 189 cbvralw xAzAyBCyz/xBCx=zwAzAyw/xBCyz/xBCw=z
191 sbsbc zwyw/xBC[˙z/w]˙yw/xBC
192 sbcel2 [˙z/w]˙yw/xBCyz/ww/xBC
193 csbin z/ww/xBC=z/ww/xBz/wC
194 csbcow z/ww/xB=z/xB
195 csbconstg zVz/wC=C
196 195 elv z/wC=C
197 194 196 ineq12i z/ww/xBz/wC=z/xBC
198 193 197 eqtri z/ww/xBC=z/xBC
199 198 eleq2i yz/ww/xBCyz/xBC
200 191 192 199 3bitrri yz/xBCzwyw/xBC
201 200 anbi2i yw/xBCyz/xBCyw/xBCzwyw/xBC
202 201 imbi1i yw/xBCyz/xBCw=zyw/xBCzwyw/xBCw=z
203 202 2ralbii wAzAyw/xBCyz/xBCw=zwAzAyw/xBCzwyw/xBCw=z
204 178 190 203 3bitri xAwAyBCwxyBCx=wwAzAyw/xBCzwyw/xBCw=z
205 94 204 sylib φyranxABCwAzAyw/xBCzwyw/xBCw=z
206 160 152 205 syl2anc φwAyw/xBCwAzAyw/xBCzwyw/xBCw=z
207 reu2 ∃!wAyw/xBCwAyw/xBCwAzAyw/xBCzwyw/xBCw=z
208 159 206 207 sylanbrc φwAyw/xBC∃!wAyw/xBC
209 riota1 ∃!wAyw/xBCwAyw/xBCιwA|yw/xBC=w
210 208 209 syl φwAyw/xBCwAyw/xBCιwA|yw/xBC=w
211 129 157 210 mpbi2and φwAyw/xBCιwA|yw/xBC=w
212 156 211 eqtr2id φwAyw/xBCw=ιxA|yBC
213 152 212 jca φwAyw/xBCyranxABCw=ιxA|yBC
214 213 ex φwAyw/xBCyranxABCw=ιxA|yBC
215 126 214 sylan2 φwxA|BCyw/xBCyranxABCw=ιxA|yBC
216 215 eximdv φwxA|BCyyw/xBCyyranxABCw=ιxA|yBC
217 125 216 mpd φwxA|BCyyranxABCw=ιxA|yBC
218 df-rex yranxABCw=ιxA|yBCyyranxABCw=ιxA|yBC
219 217 218 sylibr φwxA|BCyranxABCw=ιxA|yBC
220 219 ralrimiva φwxA|BCyranxABCw=ιxA|yBC
221 eqid yranxABCιxA|yBC=yranxABCιxA|yBC
222 221 fompt yranxABCιxA|yBC:ranxABContoxA|BCyranxABCιxA|yBCxA|BCwxA|BCyranxABCw=ιxA|yBC
223 115 220 222 sylanbrc φyranxABCιxA|yBC:ranxABContoxA|BC
224 fodomg ranxABCVyranxABCιxA|yBC:ranxABContoxA|BCxA|BCranxABC
225 8 223 224 sylc φxA|BCranxABC
226 domfi ranxABCFinxA|BCranxABCxA|BCFin
227 6 225 226 syl2anc φxA|BCFin