hashgt1

Description: Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023)

		Ref	Expression
	Assertion	hashgt1	$⊢ A \in V \to (\neg A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow 1 < \|A\|)$

Step	Hyp	Ref	Expression
1		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
2		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
3		elpreima	$⊢ \|.\| Fn V \to (A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow (A \in V \land \|A\| \in \{0, 1\}))$
4	1 2 3	mp2b	$⊢ A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow (A \in V \land \|A\| \in \{0, 1\})$
5		elex	$⊢ A \in V \to A \in V$
6	5	biantrurd	$⊢ A \in V \to (\|A\| \in \{0, 1\} \leftrightarrow (A \in V \land \|A\| \in \{0, 1\}))$
7	4 6	bitr4id	$⊢ A \in V \to (A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow \|A\| \in \{0, 1\})$
8	7	notbid	$⊢ A \in V \to (\neg A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow \neg \|A\| \in \{0, 1\})$
9		hashxnn0	$⊢ A \in V \to \|A\| \in ℕ_{0}^{*}$
10		xnn01gt	$⊢ \|A\| \in ℕ_{0}^{*} \to (\neg \|A\| \in \{0, 1\} \leftrightarrow 1 < \|A\|)$
11	9 10	syl	$⊢ A \in V \to (\neg \|A\| \in \{0, 1\} \leftrightarrow 1 < \|A\|)$
12	8 11	bitrd	$⊢ A \in V \to (\neg A \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow 1 < \|A\|)$

Metamath Proof Explorer