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	$⊢ (\neg A \in Fin \land B \in Fin \land A \subseteq ⋃ B) \to \exists x \in B \neg A \cap x \in Fin$

Proof

Step	Hyp	Ref	Expression
1		dfral2	$⊢ \forall x \in B A \cap x \in Fin \leftrightarrow \neg \exists x \in B \neg A \cap x \in Fin$
2		iunfi	$⊢ (B \in Fin \land \forall x \in B A \cap x \in Fin) \to ⋃_{x \in B} (A \cap x) \in Fin$
3		iunin2	$⊢ ⋃_{x \in B} (A \cap x) = A \cap ⋃_{x \in B} x$
4	3	eleq1i	$⊢ ⋃_{x \in B} (A \cap x) \in Fin \leftrightarrow A \cap ⋃_{x \in B} x \in Fin$
5		uniiun	$⊢ ⋃ B = ⋃_{x \in B} x$
6	5	eqcomi	$⊢ ⋃_{x \in B} x = ⋃ B$
7	6	ineq2i	$⊢ A \cap ⋃_{x \in B} x = A \cap ⋃ B$
8	7	eleq1i	$⊢ A \cap ⋃_{x \in B} x \in Fin \leftrightarrow A \cap ⋃ B \in Fin$
9		df-ss	$⊢ A \subseteq ⋃ B \leftrightarrow A \cap ⋃ B = A$
10		eleq1	$⊢ A \cap ⋃ B = A \to (A \cap ⋃ B \in Fin \leftrightarrow A \in Fin)$
11		pm2.24	$⊢ A \in Fin \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin)$
12	10 11	syl6bi	$⊢ A \cap ⋃ B = A \to (A \cap ⋃ B \in Fin \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
13	9 12	sylbi	$⊢ A \subseteq ⋃ B \to (A \cap ⋃ B \in Fin \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
14	13	com12	$⊢ A \cap ⋃ B \in Fin \to (A \subseteq ⋃ B \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
15	8 14	sylbi	$⊢ A \cap ⋃_{x \in B} x \in Fin \to (A \subseteq ⋃ B \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
16	4 15	sylbi	$⊢ ⋃_{x \in B} (A \cap x) \in Fin \to (A \subseteq ⋃ B \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
17	2 16	syl	$⊢ (B \in Fin \land \forall x \in B A \cap x \in Fin) \to (A \subseteq ⋃ B \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin))$
18	17	ex	$⊢ B \in Fin \to (\forall x \in B A \cap x \in Fin \to (A \subseteq ⋃ B \to (\neg A \in Fin \to \exists x \in B \neg A \cap x \in Fin)))$
19	18	com24	$⊢ B \in Fin \to (\neg A \in Fin \to (A \subseteq ⋃ B \to (\forall x \in B A \cap x \in Fin \to \exists x \in B \neg A \cap x \in Fin)))$
20	19	3imp21	$⊢ (\neg A \in Fin \land B \in Fin \land A \subseteq ⋃ B) \to (\forall x \in B A \cap x \in Fin \to \exists x \in B \neg A \cap x \in Fin)$
21	1 20	biimtrrid	$⊢ (\neg A \in Fin \land B \in Fin \land A \subseteq ⋃ B) \to (\neg \exists x \in B \neg A \cap x \in Fin \to \exists x \in B \neg A \cap x \in Fin)$
22	21	pm2.18d	$⊢ (\neg A \in Fin \land B \in Fin \land A \subseteq ⋃ B) \to \exists x \in B \neg A \cap x \in Fin$

Metamath Proof Explorer

Theorem infssuni

Proof