Metamath Proof Explorer


Theorem fissuni

Description: A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion fissuni ABAFinc𝒫BFinAc

Proof

Step Hyp Ref Expression
1 simpr ABAFinAFin
2 dfss3 ABxAxB
3 eluni2 xBzBxz
4 3 ralbii xAxBxAzBxz
5 2 4 sylbb ABxAzBxz
6 5 adantr ABAFinxAzBxz
7 eleq2 z=fxxzxfx
8 7 ac6sfi AFinxAzBxzff:ABxAxfx
9 1 6 8 syl2anc ABAFinff:ABxAxfx
10 fimass f:ABfAB
11 vex fV
12 11 imaex fAV
13 12 elpw fA𝒫BfAB
14 10 13 sylibr f:ABfA𝒫B
15 14 ad2antrl ABAFinf:ABxAxfxfA𝒫B
16 ffun f:ABFunf
17 16 ad2antrl ABAFinf:ABxAxfxFunf
18 simplr ABAFinf:ABxAxfxAFin
19 imafi FunfAFinfAFin
20 17 18 19 syl2anc ABAFinf:ABxAxfxfAFin
21 15 20 elind ABAFinf:ABxAxfxfA𝒫BFin
22 ffn f:ABfFnA
23 22 adantr f:ABxAfFnA
24 ssidd f:ABxAAA
25 simpr f:ABxAxA
26 fnfvima fFnAAAxAfxfA
27 23 24 25 26 syl3anc f:ABxAfxfA
28 elssuni fxfAfxfA
29 27 28 syl f:ABxAfxfA
30 29 sseld f:ABxAxfxxfA
31 30 ralimdva f:ABxAxfxxAxfA
32 31 imp f:ABxAxfxxAxfA
33 dfss3 AfAxAxfA
34 32 33 sylibr f:ABxAxfxAfA
35 34 adantl ABAFinf:ABxAxfxAfA
36 unieq c=fAc=fA
37 36 sseq2d c=fAAcAfA
38 37 rspcev fA𝒫BFinAfAc𝒫BFinAc
39 21 35 38 syl2anc ABAFinf:ABxAxfxc𝒫BFinAc
40 9 39 exlimddv ABAFinc𝒫BFinAc