Theorem 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	⊢ ( 𝜑 → 𝐴 ≈ ℕ )
	fiphp3d.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	fiphp3d.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
Assertion	fiphp3d	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		fiphp3d.a	⊢ ( 𝜑 → 𝐴 ≈ ℕ )
2		fiphp3d.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		fiphp3d.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
4		ominf	⊢ ¬ ω ∈ Fin
5		iunrab	⊢ ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 }
6		risset	⊢ ( 𝐷 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝐷 )
7		eqcom	⊢ ( 𝑦 = 𝐷 ↔ 𝐷 = 𝑦 )
8	7	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 = 𝐷 ↔ ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 )
9	6 8	bitri	⊢ ( 𝐷 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 )
10	3 9	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 )
11	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 )
12		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 } ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 )
13	11 12	sylibr	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝐷 = 𝑦 } )
14	5 13	eqtr4id	⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } = 𝐴 )
15	14	eleq1d	⊢ ( 𝜑 → ( ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ↔ 𝐴 ∈ Fin ) )
16		nnenom	⊢ ℕ ≈ ω
17		entr	⊢ ( ( 𝐴 ≈ ℕ ∧ ℕ ≈ ω ) → 𝐴 ≈ ω )
18	1 16 17	sylancl	⊢ ( 𝜑 → 𝐴 ≈ ω )
19		enfi	⊢ ( 𝐴 ≈ ω → ( 𝐴 ∈ Fin ↔ ω ∈ Fin ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝐴 ∈ Fin ↔ ω ∈ Fin ) )
21	15 20	bitrd	⊢ ( 𝜑 → ( ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ↔ ω ∈ Fin ) )
22	4 21	mtbiri	⊢ ( 𝜑 → ¬ ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
23		iunfi	⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
24	2 23	sylan	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
25	22 24	mtand	⊢ ( 𝜑 → ¬ ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
26		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐵 ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ↔ ¬ ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
27	25 26	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin )
28	18 16	jctir	⊢ ( 𝜑 → ( 𝐴 ≈ ω ∧ ℕ ≈ ω ) )
29		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ⊆ 𝐴
30	29	jctl	⊢ ( ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin → ( { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ⊆ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ) )
31		ctbnfien	⊢ ( ( ( 𝐴 ≈ ω ∧ ℕ ≈ ω ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ⊆ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ )
32	28 30 31	syl2an	⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ )
33	32	ex	⊢ ( 𝜑 → ( ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin → { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ ) )
34	33	reximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ¬ { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ∈ Fin → ∃ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ ) )
35	27 34	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦 } ≈ ℕ )