This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ ) )