birthdaylem1

	Ref	Expression
Hypotheses	birthday.s	$⊢ S = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
	birthday.t	$⊢ T = \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}$
Assertion	birthdaylem1	$⊢ (T \subseteq S \land S \in Fin \land (N \in ℕ \to S \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		birthday.s	$⊢ S = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
2		birthday.t	$⊢ T = \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}$
3		f1f	$⊢ f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N) \to f : (1 \dots K) ⟶ (1 \dots N)$
4	3	ss2abi	$⊢ \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} \subseteq \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
5	4 2 1	3sstr4i	$⊢ T \subseteq S$
6		fzfi	$⊢ (1 \dots N) \in Fin$
7		fzfi	$⊢ (1 \dots K) \in Fin$
8		mapvalg	$⊢ ((1 \dots N) \in Fin \land (1 \dots K) \in Fin) \to {(1 \dots N)}^{(1 \dots K)} = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
9	6 7 8	mp2an	$⊢ {(1 \dots N)}^{(1 \dots K)} = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
10	1 9	eqtr4i	$⊢ S = {(1 \dots N)}^{(1 \dots K)}$
11		mapfi	$⊢ ((1 \dots N) \in Fin \land (1 \dots K) \in Fin) \to {(1 \dots N)}^{(1 \dots K)} \in Fin$
12	6 7 11	mp2an	$⊢ {(1 \dots N)}^{(1 \dots K)} \in Fin$
13	10 12	eqeltri	$⊢ S \in Fin$
14		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
15		ne0i	$⊢ N \in (1 \dots N) \to (1 \dots N) \neq \emptyset$
16	14 15	sylbi	$⊢ N \in ℕ \to (1 \dots N) \neq \emptyset$
17	10	eqeq1i	$⊢ S = \emptyset \leftrightarrow {(1 \dots N)}^{(1 \dots K)} = \emptyset$
18		ovex	$⊢ (1 \dots N) \in V$
19		ovex	$⊢ (1 \dots K) \in V$
20	18 19	map0	$⊢ {(1 \dots N)}^{(1 \dots K)} = \emptyset \leftrightarrow ((1 \dots N) = \emptyset \land (1 \dots K) \neq \emptyset)$
21	20	simplbi	$⊢ {(1 \dots N)}^{(1 \dots K)} = \emptyset \to (1 \dots N) = \emptyset$
22	17 21	sylbi	$⊢ S = \emptyset \to (1 \dots N) = \emptyset$
23	22	necon3i	$⊢ (1 \dots N) \neq \emptyset \to S \neq \emptyset$
24	16 23	syl	$⊢ N \in ℕ \to S \neq \emptyset$
25	5 13 24	3pm3.2i	$⊢ (T \subseteq S \land S \in Fin \land (N \in ℕ \to S \neq \emptyset))$

Metamath Proof Explorer

Theorem birthdaylem1

Proof