fiphp3d

Description: Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014)

	Ref	Expression
Hypotheses	fiphp3d.a	$⊢ φ \to A \approx ℕ$
	fiphp3d.b	$⊢ φ \to B \in Fin$
	fiphp3d.c	$⊢ (φ \land x \in A) \to D \in B$
Assertion	fiphp3d	$⊢ φ \to \exists y \in B \{x \in A \| D = y\} \approx ℕ$

Proof

Step	Hyp	Ref	Expression
1		fiphp3d.a	$⊢ φ \to A \approx ℕ$
2		fiphp3d.b	$⊢ φ \to B \in Fin$
3		fiphp3d.c	$⊢ (φ \land x \in A) \to D \in B$
4		ominf	$⊢ \neg ω \in Fin$
5		iunrab	$⊢ ⋃_{y \in B} \{x \in A \| D = y\} = \{x \in A \| \exists y \in B D = y\}$
6		risset	$⊢ D \in B \leftrightarrow \exists y \in B y = D$
7		eqcom	$⊢ y = D \leftrightarrow D = y$
8	7	rexbii	$⊢ \exists y \in B y = D \leftrightarrow \exists y \in B D = y$
9	6 8	bitri	$⊢ D \in B \leftrightarrow \exists y \in B D = y$
10	3 9	sylib	$⊢ (φ \land x \in A) \to \exists y \in B D = y$
11	10	ralrimiva	$⊢ φ \to \forall x \in A \exists y \in B D = y$
12		rabid2	$⊢ A = \{x \in A \| \exists y \in B D = y\} \leftrightarrow \forall x \in A \exists y \in B D = y$
13	11 12	sylibr	$⊢ φ \to A = \{x \in A \| \exists y \in B D = y\}$
14	5 13	eqtr4id	$⊢ φ \to ⋃_{y \in B} \{x \in A \| D = y\} = A$
15	14	eleq1d	$⊢ φ \to (⋃_{y \in B} \{x \in A \| D = y\} \in Fin \leftrightarrow A \in Fin)$
16		nnenom	$⊢ ℕ \approx ω$
17		entr	$⊢ (A \approx ℕ \land ℕ \approx ω) \to A \approx ω$
18	1 16 17	sylancl	$⊢ φ \to A \approx ω$
19		enfi	$⊢ A \approx ω \to (A \in Fin \leftrightarrow ω \in Fin)$
20	18 19	syl	$⊢ φ \to (A \in Fin \leftrightarrow ω \in Fin)$
21	15 20	bitrd	$⊢ φ \to (⋃_{y \in B} \{x \in A \| D = y\} \in Fin \leftrightarrow ω \in Fin)$
22	4 21	mtbiri	$⊢ φ \to \neg ⋃_{y \in B} \{x \in A \| D = y\} \in Fin$
23		iunfi	$⊢ (B \in Fin \land \forall y \in B \{x \in A \| D = y\} \in Fin) \to ⋃_{y \in B} \{x \in A \| D = y\} \in Fin$
24	2 23	sylan	$⊢ (φ \land \forall y \in B \{x \in A \| D = y\} \in Fin) \to ⋃_{y \in B} \{x \in A \| D = y\} \in Fin$
25	22 24	mtand	$⊢ φ \to \neg \forall y \in B \{x \in A \| D = y\} \in Fin$
26		rexnal	$⊢ \exists y \in B \neg \{x \in A \| D = y\} \in Fin \leftrightarrow \neg \forall y \in B \{x \in A \| D = y\} \in Fin$
27	25 26	sylibr	$⊢ φ \to \exists y \in B \neg \{x \in A \| D = y\} \in Fin$
28	18 16	jctir	$⊢ φ \to (A \approx ω \land ℕ \approx ω)$
29		ssrab2	$⊢ \{x \in A \| D = y\} \subseteq A$
30	29	jctl	$⊢ \neg \{x \in A \| D = y\} \in Fin \to (\{x \in A \| D = y\} \subseteq A \land \neg \{x \in A \| D = y\} \in Fin)$
31		ctbnfien	$⊢ ((A \approx ω \land ℕ \approx ω) \land (\{x \in A \| D = y\} \subseteq A \land \neg \{x \in A \| D = y\} \in Fin)) \to \{x \in A \| D = y\} \approx ℕ$
32	28 30 31	syl2an	$⊢ (φ \land \neg \{x \in A \| D = y\} \in Fin) \to \{x \in A \| D = y\} \approx ℕ$
33	32	ex	$⊢ φ \to (\neg \{x \in A \| D = y\} \in Fin \to \{x \in A \| D = y\} \approx ℕ)$
34	33	reximdv	$⊢ φ \to (\exists y \in B \neg \{x \in A \| D = y\} \in Fin \to \exists y \in B \{x \in A \| D = y\} \approx ℕ)$
35	27 34	mpd	$⊢ φ \to \exists y \in B \{x \in A \| D = y\} \approx ℕ$

Metamath Proof Explorer

Theorem fiphp3d

Proof