sticksstones4

Description: Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024)

	Ref	Expression
Hypotheses	sticksstones4.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones4.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones4.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
	sticksstones4.4	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
Assertion	sticksstones4	$⊢ φ \to A \approx B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones4.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones4.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones4.3	$⊢ B = \{a \in 𝒫 (1 \dots N) \| \|a\| = K\}$
4		sticksstones4.4	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
5		eqid	$⊢ (p \in A ⟼ ran p) = (p \in A ⟼ ran p)$
6	1 2 3 4 5	sticksstones2	$⊢ φ \to (p \in A ⟼ ran p) : A \underset{1-1}{⟶} B$
7	1 2 3 4 5	sticksstones3	$⊢ φ \to (p \in A ⟼ ran p) : A \underset{onto}{⟶} B$
8	6 7	jca	$⊢ φ \to ((p \in A ⟼ ran p) : A \underset{1-1}{⟶} B \land (p \in A ⟼ ran p) : A \underset{onto}{⟶} B)$
9		df-f1o	$⊢ (p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B \leftrightarrow ((p \in A ⟼ ran p) : A \underset{1-1}{⟶} B \land (p \in A ⟼ ran p) : A \underset{onto}{⟶} B)$
10	8 9	sylibr	$⊢ φ \to (p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B$
11		simpl	$⊢ (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \to f : (1 \dots K) ⟶ (1 \dots N)$
12	11	a1i	$⊢ φ \to ((f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \to f : (1 \dots K) ⟶ (1 \dots N))$
13	12	ss2abdv	$⊢ φ \to \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \subseteq \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
14		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
15		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
16		mapex	$⊢ ((1 \dots K) \in Fin \land (1 \dots N) \in Fin) \to \{f \| f : (1 \dots K) ⟶ (1 \dots N)\} \in V$
17	14 15 16	syl2anc	$⊢ φ \to \{f \| f : (1 \dots K) ⟶ (1 \dots N)\} \in V$
18		ssexg	$⊢ (\{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \subseteq \{f \| f : (1 \dots K) ⟶ (1 \dots N)\} \land \{f \| f : (1 \dots K) ⟶ (1 \dots N)\} \in V) \to \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \in V$
19	13 17 18	syl2anc	$⊢ φ \to \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \in V$
20	4	eleq1i	$⊢ A \in V \leftrightarrow \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \in V$
21	19 20	sylibr	$⊢ φ \to A \in V$
22	21	mptexd	$⊢ φ \to (p \in A ⟼ ran p) \in V$
23		f1oeq1	$⊢ g = (p \in A ⟼ ran p) \to (g : A \underset{1-1 onto}{⟶} B \leftrightarrow (p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B)$
24	23	biimprd	$⊢ g = (p \in A ⟼ ran p) \to ((p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B \to g : A \underset{1-1 onto}{⟶} B)$
25	24	adantl	$⊢ (φ \land g = (p \in A ⟼ ran p)) \to ((p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B \to g : A \underset{1-1 onto}{⟶} B)$
26	22 25	spcimedv	$⊢ φ \to ((p \in A ⟼ ran p) : A \underset{1-1 onto}{⟶} B \to \exists g g : A \underset{1-1 onto}{⟶} B)$
27	10 26	mpd	$⊢ φ \to \exists g g : A \underset{1-1 onto}{⟶} B$
28		bren	$⊢ A \approx B \leftrightarrow \exists g g : A \underset{1-1 onto}{⟶} B$
29	27 28	sylibr	$⊢ φ \to A \approx B$

Metamath Proof Explorer

Theorem sticksstones4

Proof