Metamath Proof Explorer

Theorem hashres

Description: The number of elements of a finite function restricted to a subset of its domain is equal to the number of elements of that subset. (Contributed by AV, 15-Dec-2021)

		Ref	Expression
	Assertion	hashres	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to \|{A ↾}_{B}\| = \|B\|$

Proof

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun A \to Fun ({A ↾}_{B})$
2	1	3ad2ant1	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to Fun ({A ↾}_{B})$
3		finresfin	$⊢ A \in Fin \to {A ↾}_{B} \in Fin$
4	3	3ad2ant2	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to {A ↾}_{B} \in Fin$
5		hashfun	$⊢ {A ↾}_{B} \in Fin \to (Fun ({A ↾}_{B}) \leftrightarrow \|{A ↾}_{B}\| = \|dom ({A ↾}_{B})\|)$
6	4 5	syl	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to (Fun ({A ↾}_{B}) \leftrightarrow \|{A ↾}_{B}\| = \|dom ({A ↾}_{B})\|)$
7	2 6	mpbid	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to \|{A ↾}_{B}\| = \|dom ({A ↾}_{B})\|$
8		ssdmres	$⊢ B \subseteq dom A \leftrightarrow dom ({A ↾}_{B}) = B$
9	8	biimpi	$⊢ B \subseteq dom A \to dom ({A ↾}_{B}) = B$
10	9	3ad2ant3	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to dom ({A ↾}_{B}) = B$
11	10	fveq2d	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to \|dom ({A ↾}_{B})\| = \|B\|$
12	7 11	eqtrd	$⊢ (Fun A \land A \in Fin \land B \subseteq dom A) \to \|{A ↾}_{B}\| = \|B\|$