hashsnle1

Description: The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021)

		Ref	Expression
	Assertion	hashsnle1	$⊢ \|\{A\}\| \leq 1$

Step	Hyp	Ref	Expression
1		hashsn01	$⊢ (\|\{A\}\| = 0 \lor \|\{A\}\| = 1)$
2		0le1	$⊢ 0 \leq 1$
3		breq1	$⊢ \|\{A\}\| = 0 \to (\|\{A\}\| \leq 1 \leftrightarrow 0 \leq 1)$
4	2 3	mpbiri	$⊢ \|\{A\}\| = 0 \to \|\{A\}\| \leq 1$
5		1le1	$⊢ 1 \leq 1$
6		breq1	$⊢ \|\{A\}\| = 1 \to (\|\{A\}\| \leq 1 \leftrightarrow 1 \leq 1)$
7	5 6	mpbiri	$⊢ \|\{A\}\| = 1 \to \|\{A\}\| \leq 1$
8	4 7	jaoi	$⊢ (\|\{A\}\| = 0 \lor \|\{A\}\| = 1) \to \|\{A\}\| \leq 1$
9	1 8	ax-mp	$⊢ \|\{A\}\| \leq 1$

Metamath Proof Explorer