hashsng

Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 13-Feb-2013)

		Ref	Expression
	Assertion	hashsng	$⊢ A \in V \to \|\{A\}\| = 1$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		en2sn	$⊢ (A \in V \land 1 \in ℤ) \to \{A\} \approx \{1\}$
3	1 2	mpan2	$⊢ A \in V \to \{A\} \approx \{1\}$
4		snfi	$⊢ \{A\} \in Fin$
5		snfi	$⊢ \{1\} \in Fin$
6		hashen	$⊢ (\{A\} \in Fin \land \{1\} \in Fin) \to (\|\{A\}\| = \|\{1\}\| \leftrightarrow \{A\} \approx \{1\})$
7	4 5 6	mp2an	$⊢ \|\{A\}\| = \|\{1\}\| \leftrightarrow \{A\} \approx \{1\}$
8	3 7	sylibr	$⊢ A \in V \to \|\{A\}\| = \|\{1\}\|$
9		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
10	9	fveq2d	$⊢ 1 \in ℤ \to \|(1 \dots 1)\| = \|\{1\}\|$
11		1nn0	$⊢ 1 \in ℕ_{0}$
12		hashfz1	$⊢ 1 \in ℕ_{0} \to \|(1 \dots 1)\| = 1$
13	11 12	ax-mp	$⊢ \|(1 \dots 1)\| = 1$
14	10 13	eqtr3di	$⊢ 1 \in ℤ \to \|\{1\}\| = 1$
15	1 14	ax-mp	$⊢ \|\{1\}\| = 1$
16	8 15	eqtrdi	$⊢ A \in V \to \|\{A\}\| = 1$

Metamath Proof Explorer