Metamath Proof Explorer

Theorem infssuni

Description: If an infinite set A is included in the underlying set of a finite cover B , then there exists a set of the cover that contains an infinite number of element of A . (Contributed by FL, 2-Aug-2009)

Ref Expression
Assertion infssuni 
|- ( ( -. A e. Fin /\ B e. Fin /\ A C_ U. B ) -> E. x e. B -. ( A i^i x ) e. Fin )

Proof

Step Hyp Ref Expression
1 dfral2 
 |-  ( A. x e. B ( A i^i x ) e. Fin <-> -. E. x e. B -. ( A i^i x ) e. Fin )
2 iunfi 
 |-  ( ( B e. Fin /\ A. x e. B ( A i^i x ) e. Fin ) -> U_ x e. B ( A i^i x ) e. Fin )
3 iunin2 
 |-  U_ x e. B ( A i^i x ) = ( A i^i U_ x e. B x )
4 3 eleq1i 
 |-  ( U_ x e. B ( A i^i x ) e. Fin <-> ( A i^i U_ x e. B x ) e. Fin )
5 uniiun 
 |-  U. B = U_ x e. B x
6 5 eqcomi 
 |-  U_ x e. B x = U. B
7 6 ineq2i 
 |-  ( A i^i U_ x e. B x ) = ( A i^i U. B )
8 7 eleq1i 
 |-  ( ( A i^i U_ x e. B x ) e. Fin <-> ( A i^i U. B ) e. Fin )
9 df-ss 
 |-  ( A C_ U. B <-> ( A i^i U. B ) = A )
10 eleq1 
 |-  ( ( A i^i U. B ) = A -> ( ( A i^i U. B ) e. Fin <-> A e. Fin ) )
11 pm2.24 
 |-  ( A e. Fin -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) )
12 10 11 syl6bi 
 |-  ( ( A i^i U. B ) = A -> ( ( A i^i U. B ) e. Fin -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
13 9 12 sylbi 
 |-  ( A C_ U. B -> ( ( A i^i U. B ) e. Fin -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
14 13 com12 
 |-  ( ( A i^i U. B ) e. Fin -> ( A C_ U. B -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
15 8 14 sylbi 
 |-  ( ( A i^i U_ x e. B x ) e. Fin -> ( A C_ U. B -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
16 4 15 sylbi 
 |-  ( U_ x e. B ( A i^i x ) e. Fin -> ( A C_ U. B -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
17 2 16 syl 
 |-  ( ( B e. Fin /\ A. x e. B ( A i^i x ) e. Fin ) -> ( A C_ U. B -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) )
18 17 ex 
 |-  ( B e. Fin -> ( A. x e. B ( A i^i x ) e. Fin -> ( A C_ U. B -> ( -. A e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) ) )
19 18 com24 
 |-  ( B e. Fin -> ( -. A e. Fin -> ( A C_ U. B -> ( A. x e. B ( A i^i x ) e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) ) ) )
20 19 3imp21 
 |-  ( ( -. A e. Fin /\ B e. Fin /\ A C_ U. B ) -> ( A. x e. B ( A i^i x ) e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) )
21 1 20 syl5bir 
 |-  ( ( -. A e. Fin /\ B e. Fin /\ A C_ U. B ) -> ( -. E. x e. B -. ( A i^i x ) e. Fin -> E. x e. B -. ( A i^i x ) e. Fin ) )
22 21 pm2.18d 
 |-  ( ( -. A e. Fin /\ B e. Fin /\ A C_ U. B ) -> E. x e. B -. ( A i^i x ) e. Fin )