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 
|- ( ( A C_ U. B /\ A e. Fin ) -> E. c e. ( ~P B i^i Fin ) A C_ U. c )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A C_ U. B /\ A e. Fin ) -> A e. Fin )
2 dfss3 
 |-  ( A C_ U. B <-> A. x e. A x e. U. B )
3 eluni2 
 |-  ( x e. U. B <-> E. z e. B x e. z )
4 3 ralbii 
 |-  ( A. x e. A x e. U. B <-> A. x e. A E. z e. B x e. z )
5 2 4 sylbb 
 |-  ( A C_ U. B -> A. x e. A E. z e. B x e. z )
6 5 adantr 
 |-  ( ( A C_ U. B /\ A e. Fin ) -> A. x e. A E. z e. B x e. z )
7 eleq2 
 |-  ( z = ( f ` x ) -> ( x e. z <-> x e. ( f ` x ) ) )
8 7 ac6sfi 
 |-  ( ( A e. Fin /\ A. x e. A E. z e. B x e. z ) -> E. f ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) )
9 1 6 8 syl2anc 
 |-  ( ( A C_ U. B /\ A e. Fin ) -> E. f ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) )
10 fimass 
 |-  ( f : A --> B -> ( f " A ) C_ B )
11 vex 
 |-  f e. _V
12 11 imaex 
 |-  ( f " A ) e. _V
13 12 elpw 
 |-  ( ( f " A ) e. ~P B <-> ( f " A ) C_ B )
14 10 13 sylibr 
 |-  ( f : A --> B -> ( f " A ) e. ~P B )
15 14 ad2antrl 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> ( f " A ) e. ~P B )
16 ffun 
 |-  ( f : A --> B -> Fun f )
17 16 ad2antrl 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> Fun f )
18 simplr 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> A e. Fin )
19 imafi 
 |-  ( ( Fun f /\ A e. Fin ) -> ( f " A ) e. Fin )
20 17 18 19 syl2anc 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> ( f " A ) e. Fin )
21 15 20 elind 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> ( f " A ) e. ( ~P B i^i Fin ) )
22 ffn 
 |-  ( f : A --> B -> f Fn A )
23 22 adantr 
 |-  ( ( f : A --> B /\ x e. A ) -> f Fn A )
24 ssidd 
 |-  ( ( f : A --> B /\ x e. A ) -> A C_ A )
25 simpr 
 |-  ( ( f : A --> B /\ x e. A ) -> x e. A )
26 fnfvima 
 |-  ( ( f Fn A /\ A C_ A /\ x e. A ) -> ( f ` x ) e. ( f " A ) )
27 23 24 25 26 syl3anc 
 |-  ( ( f : A --> B /\ x e. A ) -> ( f ` x ) e. ( f " A ) )
28 elssuni 
 |-  ( ( f ` x ) e. ( f " A ) -> ( f ` x ) C_ U. ( f " A ) )
29 27 28 syl 
 |-  ( ( f : A --> B /\ x e. A ) -> ( f ` x ) C_ U. ( f " A ) )
30 29 sseld 
 |-  ( ( f : A --> B /\ x e. A ) -> ( x e. ( f ` x ) -> x e. U. ( f " A ) ) )
31 30 ralimdva 
 |-  ( f : A --> B -> ( A. x e. A x e. ( f ` x ) -> A. x e. A x e. U. ( f " A ) ) )
32 31 imp 
 |-  ( ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) -> A. x e. A x e. U. ( f " A ) )
33 dfss3 
 |-  ( A C_ U. ( f " A ) <-> A. x e. A x e. U. ( f " A ) )
34 32 33 sylibr 
 |-  ( ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) -> A C_ U. ( f " A ) )
35 34 adantl 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> A C_ U. ( f " A ) )
36 unieq 
 |-  ( c = ( f " A ) -> U. c = U. ( f " A ) )
37 36 sseq2d 
 |-  ( c = ( f " A ) -> ( A C_ U. c <-> A C_ U. ( f " A ) ) )
38 37 rspcev 
 |-  ( ( ( f " A ) e. ( ~P B i^i Fin ) /\ A C_ U. ( f " A ) ) -> E. c e. ( ~P B i^i Fin ) A C_ U. c )
39 21 35 38 syl2anc 
 |-  ( ( ( A C_ U. B /\ A e. Fin ) /\ ( f : A --> B /\ A. x e. A x e. ( f ` x ) ) ) -> E. c e. ( ~P B i^i Fin ) A C_ U. c )
40 9 39 exlimddv 
 |-  ( ( A C_ U. B /\ A e. Fin ) -> E. c e. ( ~P B i^i Fin ) A C_ U. c )