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 Fin B Fin A B x B ¬ A x Fin

Proof

Step Hyp Ref Expression
1 dfral2 x B A x Fin ¬ x B ¬ A x Fin
2 iunfi B Fin x B A x Fin x B A x Fin
3 iunin2 x B A x = A x B x
4 3 eleq1i x B A x Fin A x B x Fin
5 uniiun B = x B x
6 5 eqcomi x B x = B
7 6 ineq2i A x B x = A B
8 7 eleq1i A x B x Fin A B Fin
9 df-ss A B A B = A
10 eleq1 A B = A A B Fin A Fin
11 pm2.24 A Fin ¬ A Fin x B ¬ A x Fin
12 10 11 syl6bi A B = A A B Fin ¬ A Fin x B ¬ A x Fin
13 9 12 sylbi A B A B Fin ¬ A Fin x B ¬ A x Fin
14 13 com12 A B Fin A B ¬ A Fin x B ¬ A x Fin
15 8 14 sylbi A x B x Fin A B ¬ A Fin x B ¬ A x Fin
16 4 15 sylbi x B A x Fin A B ¬ A Fin x B ¬ A x Fin
17 2 16 syl B Fin x B A x Fin A B ¬ A Fin x B ¬ A x Fin
18 17 ex B Fin x B A x Fin A B ¬ A Fin x B ¬ A x Fin
19 18 com24 B Fin ¬ A Fin A B x B A x Fin x B ¬ A x Fin
20 19 3imp21 ¬ A Fin B Fin A B x B A x Fin x B ¬ A x Fin
21 1 20 syl5bir ¬ A Fin B Fin A B ¬ x B ¬ A x Fin x B ¬ A x Fin
22 21 pm2.18d ¬ A Fin B Fin A B x B ¬ A x Fin