hashge2el2dif

Description: A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019)

		Ref	Expression
	Assertion	hashge2el2dif	$⊢ (D \in V \land 2 \leq \|D\|) \to \exists x \in D \exists y \in D x \neq y$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ D = \{x\} \to \|D\| = \|\{x\}\|$
2		hashsng	$⊢ x \in D \to \|\{x\}\| = 1$
3	1 2	sylan9eqr	$⊢ (x \in D \land D = \{x\}) \to \|D\| = 1$
4	3	ralimiaa	$⊢ \forall x \in D D = \{x\} \to \forall x \in D \|D\| = 1$
5		0re	$⊢ 0 \in ℝ$
6		1re	$⊢ 1 \in ℝ$
7	5 6	readdcli	$⊢ 0 + 1 \in ℝ$
8	7	a1i	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to 0 + 1 \in ℝ$
9		2re	$⊢ 2 \in ℝ$
10	9	a1i	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to 2 \in ℝ$
11		hashcl	$⊢ D \in Fin \to \|D\| \in ℕ_{0}$
12	11	nn0red	$⊢ D \in Fin \to \|D\| \in ℝ$
13	12	adantr	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to \|D\| \in ℝ$
14	8 10 13	3jca	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (0 + 1 \in ℝ \land 2 \in ℝ \land \|D\| \in ℝ)$
15		0p1e1	$⊢ 0 + 1 = 1$
16		1lt2	$⊢ 1 < 2$
17	15 16	eqbrtri	$⊢ 0 + 1 < 2$
18	17	jctl	$⊢ 2 \leq \|D\| \to (0 + 1 < 2 \land 2 \leq \|D\|)$
19	18	adantl	$⊢ (D \in V \land 2 \leq \|D\|) \to (0 + 1 < 2 \land 2 \leq \|D\|)$
20	19	adantl	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (0 + 1 < 2 \land 2 \leq \|D\|)$
21		ltleletr	$⊢ (0 + 1 \in ℝ \land 2 \in ℝ \land \|D\| \in ℝ) \to ((0 + 1 < 2 \land 2 \leq \|D\|) \to 0 + 1 \leq \|D\|)$
22	14 20 21	sylc	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to 0 + 1 \leq \|D\|$
23	11	nn0zd	$⊢ D \in Fin \to \|D\| \in ℤ$
24		0z	$⊢ 0 \in ℤ$
25	23 24	jctil	$⊢ D \in Fin \to (0 \in ℤ \land \|D\| \in ℤ)$
26	25	adantr	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (0 \in ℤ \land \|D\| \in ℤ)$
27		zltp1le	$⊢ (0 \in ℤ \land \|D\| \in ℤ) \to (0 < \|D\| \leftrightarrow 0 + 1 \leq \|D\|)$
28	26 27	syl	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (0 < \|D\| \leftrightarrow 0 + 1 \leq \|D\|)$
29	22 28	mpbird	$⊢ (D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to 0 < \|D\|$
30		0ltpnf	$⊢ 0 < +∞$
31		simpl	$⊢ (D \in V \land 2 \leq \|D\|) \to D \in V$
32	31	anim2i	$⊢ (\neg D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (\neg D \in Fin \land D \in V)$
33	32	ancomd	$⊢ (\neg D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to (D \in V \land \neg D \in Fin)$
34		hashinf	$⊢ (D \in V \land \neg D \in Fin) \to \|D\| = +∞$
35	33 34	syl	$⊢ (\neg D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to \|D\| = +∞$
36	30 35	breqtrrid	$⊢ (\neg D \in Fin \land (D \in V \land 2 \leq \|D\|)) \to 0 < \|D\|$
37	29 36	pm2.61ian	$⊢ (D \in V \land 2 \leq \|D\|) \to 0 < \|D\|$
38		hashgt0n0	$⊢ (D \in V \land 0 < \|D\|) \to D \neq \emptyset$
39	37 38	syldan	$⊢ (D \in V \land 2 \leq \|D\|) \to D \neq \emptyset$
40		rspn0	$⊢ D \neq \emptyset \to (\forall x \in D \|D\| = 1 \to \|D\| = 1)$
41	39 40	syl	$⊢ (D \in V \land 2 \leq \|D\|) \to (\forall x \in D \|D\| = 1 \to \|D\| = 1)$
42		breq2	$⊢ \|D\| = 1 \to (2 \leq \|D\| \leftrightarrow 2 \leq 1)$
43	6 9	ltnlei	$⊢ 1 < 2 \leftrightarrow \neg 2 \leq 1$
44		pm2.21	$⊢ \neg 2 \leq 1 \to (2 \leq 1 \to \neg \forall x \in D D = \{x\})$
45	43 44	sylbi	$⊢ 1 < 2 \to (2 \leq 1 \to \neg \forall x \in D D = \{x\})$
46	16 45	ax-mp	$⊢ 2 \leq 1 \to \neg \forall x \in D D = \{x\}$
47	42 46	syl6bi	$⊢ \|D\| = 1 \to (2 \leq \|D\| \to \neg \forall x \in D D = \{x\})$
48	47	com12	$⊢ 2 \leq \|D\| \to (\|D\| = 1 \to \neg \forall x \in D D = \{x\})$
49	48	adantl	$⊢ (D \in V \land 2 \leq \|D\|) \to (\|D\| = 1 \to \neg \forall x \in D D = \{x\})$
50	41 49	syldc	$⊢ \forall x \in D \|D\| = 1 \to ((D \in V \land 2 \leq \|D\|) \to \neg \forall x \in D D = \{x\})$
51	4 50	syl	$⊢ \forall x \in D D = \{x\} \to ((D \in V \land 2 \leq \|D\|) \to \neg \forall x \in D D = \{x\})$
52		ax-1	$⊢ \neg \forall x \in D D = \{x\} \to ((D \in V \land 2 \leq \|D\|) \to \neg \forall x \in D D = \{x\})$
53	51 52	pm2.61i	$⊢ (D \in V \land 2 \leq \|D\|) \to \neg \forall x \in D D = \{x\}$
54		eqsn	$⊢ D \neq \emptyset \to (D = \{x\} \leftrightarrow \forall y \in D y = x)$
55	39 54	syl	$⊢ (D \in V \land 2 \leq \|D\|) \to (D = \{x\} \leftrightarrow \forall y \in D y = x)$
56		equcom	$⊢ y = x \leftrightarrow x = y$
57	56	a1i	$⊢ (D \in V \land 2 \leq \|D\|) \to (y = x \leftrightarrow x = y)$
58	57	ralbidv	$⊢ (D \in V \land 2 \leq \|D\|) \to (\forall y \in D y = x \leftrightarrow \forall y \in D x = y)$
59	55 58	bitrd	$⊢ (D \in V \land 2 \leq \|D\|) \to (D = \{x\} \leftrightarrow \forall y \in D x = y)$
60	59	ralbidv	$⊢ (D \in V \land 2 \leq \|D\|) \to (\forall x \in D D = \{x\} \leftrightarrow \forall x \in D \forall y \in D x = y)$
61	53 60	mtbid	$⊢ (D \in V \land 2 \leq \|D\|) \to \neg \forall x \in D \forall y \in D x = y$
62		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
63	62	rexbii	$⊢ \exists y \in D x \neq y \leftrightarrow \exists y \in D \neg x = y$
64		rexnal	$⊢ \exists y \in D \neg x = y \leftrightarrow \neg \forall y \in D x = y$
65	63 64	bitri	$⊢ \exists y \in D x \neq y \leftrightarrow \neg \forall y \in D x = y$
66	65	rexbii	$⊢ \exists x \in D \exists y \in D x \neq y \leftrightarrow \exists x \in D \neg \forall y \in D x = y$
67		rexnal	$⊢ \exists x \in D \neg \forall y \in D x = y \leftrightarrow \neg \forall x \in D \forall y \in D x = y$
68	66 67	bitri	$⊢ \exists x \in D \exists y \in D x \neq y \leftrightarrow \neg \forall x \in D \forall y \in D x = y$
69	61 68	sylibr	$⊢ (D \in V \land 2 \leq \|D\|) \to \exists x \in D \exists y \in D x \neq y$

Metamath Proof Explorer

Theorem hashge2el2dif

Proof