Theorem birthdaylem1

Description: Lemma for birthday . (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Hypotheses	birthday.s	⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
	birthday.t	⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
Assertion	birthdaylem1	⊢ ( 𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		birthday.s	⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
2		birthday.t	⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
3		f1f	⊢ ( 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) → 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
4	3	ss2abi	⊢ { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) } ⊆ { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
5	4 2 1	3sstr4i	⊢ 𝑇 ⊆ 𝑆
6		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
7		fzfi	⊢ ( 1 ... 𝐾 ) ∈ Fin
8		mapvalg	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝐾 ) ∈ Fin ) → ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } )
9	6 7 8	mp2an	⊢ ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
10	1 9	eqtr4i	⊢ 𝑆 = ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) )
11		mapfi	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝐾 ) ∈ Fin ) → ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) ∈ Fin )
12	6 7 11	mp2an	⊢ ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) ∈ Fin
13	10 12	eqeltri	⊢ 𝑆 ∈ Fin
14		elfz1end	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
15		ne0i	⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) ≠ ∅ )
16	14 15	sylbi	⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ≠ ∅ )
17	10	eqeq1i	⊢ ( 𝑆 = ∅ ↔ ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) = ∅ )
18		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
19		ovex	⊢ ( 1 ... 𝐾 ) ∈ V
20	18 19	map0	⊢ ( ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) = ∅ ↔ ( ( 1 ... 𝑁 ) = ∅ ∧ ( 1 ... 𝐾 ) ≠ ∅ ) )
21	20	simplbi	⊢ ( ( ( 1 ... 𝑁 ) ↑m ( 1 ... 𝐾 ) ) = ∅ → ( 1 ... 𝑁 ) = ∅ )
22	17 21	sylbi	⊢ ( 𝑆 = ∅ → ( 1 ... 𝑁 ) = ∅ )
23	22	necon3i	⊢ ( ( 1 ... 𝑁 ) ≠ ∅ → 𝑆 ≠ ∅ )
24	16 23	syl	⊢ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ )
25	5 13 24	3pm3.2i	⊢ ( 𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ ) )