Theorem hashge3el3dif

Description: A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif , which has an elementary proof, the dominance relation and 1-1 functions from a set with three elements which are known to be different are used to prove this theorem. Although there is also an elementary proof for this theorem, it might be much longer. After all, this proof should be kept because it can be used as template for proofs for higher cardinalities. (Contributed by AV, 20-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	hashge3el3dif	$$⊢\left(D\in V\wedge 3\le \left|D\right|\right)\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	sneqr	$$⊢\left\{\varnothing \right\}=\left\{\left\{\varnothing \right\}\right\}\to \varnothing =\left\{\varnothing \right\}$$
4	3	necon3i	$$⊢\varnothing \ne \left\{\varnothing \right\}\to \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}$$
5	1 4	ax-mp	$$⊢\left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}$$
6		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
7		snnzg	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to \left\{\left\{\varnothing \right\}\right\}\ne \varnothing$$
8	6 7	ax-mp	$$⊢\left\{\left\{\varnothing \right\}\right\}\ne \varnothing$$
9	1 5 8	3pm3.2i	$$⊢\left(\varnothing \ne \left\{\varnothing \right\}\wedge \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}\wedge \left\{\left\{\varnothing \right\}\right\}\ne \varnothing \right)$$
10		snex	$$⊢\left\{\left\{\varnothing \right\}\right\}\in \mathrm{V}$$
11	2 6 10	3pm3.2i	$$⊢\left(\varnothing \in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\wedge \left\{\left\{\varnothing \right\}\right\}\in \mathrm{V}\right)$$
12		hashtpg	$$⊢\left(\varnothing \in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\wedge \left\{\left\{\varnothing \right\}\right\}\in \mathrm{V}\right)\to \left(\left(\varnothing \ne \left\{\varnothing \right\}\wedge \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}\wedge \left\{\left\{\varnothing \right\}\right\}\ne \varnothing \right)\leftrightarrow \left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|=3\right)$$
13	11 12	ax-mp	$$⊢\left(\varnothing \ne \left\{\varnothing \right\}\wedge \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}\wedge \left\{\left\{\varnothing \right\}\right\}\ne \varnothing \right)\leftrightarrow \left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|=3$$
14	9 13	mpbi	$$⊢\left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|=3$$
15	14	eqcomi	$$⊢3=\left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|$$
16	15	a1i	$$⊢D\in V\to 3=\left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|$$
17	16	breq1d	$$⊢D\in V\to \left(3\le \left|D\right|\leftrightarrow \left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|\le \left|D\right|\right)$$
18		tpfi	$$⊢\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{Fin}$$
19		hashdom	$$⊢\left(\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{Fin}\wedge D\in V\right)\to \left(\left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|\le \left|D\right|\leftrightarrow \left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\preccurlyeq D\right)$$
20	18 19	mpan	$$⊢D\in V\to \left(\left|\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\right|\le \left|D\right|\leftrightarrow \left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\preccurlyeq D\right)$$
21	17 20	bitrd	$$⊢D\in V\to \left(3\le \left|D\right|\leftrightarrow \left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\preccurlyeq D\right)$$
22		brdomg	$$⊢D\in V\to \left(\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\preccurlyeq D\leftrightarrow \exists ff:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\right)$$
23	11	a1i	$$⊢\left(D\in V\wedge f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\right)\to \left(\varnothing \in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\wedge \left\{\left\{\varnothing \right\}\right\}\in \mathrm{V}\right)$$
24	7	necomd	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to \varnothing \ne \left\{\left\{\varnothing \right\}\right\}$$
25	6 24	ax-mp	$$⊢\varnothing \ne \left\{\left\{\varnothing \right\}\right\}$$
26	1 25 5	3pm3.2i	$$⊢\left(\varnothing \ne \left\{\varnothing \right\}\wedge \varnothing \ne \left\{\left\{\varnothing \right\}\right\}\wedge \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}\right)$$
27	26	a1i	$$⊢\left(D\in V\wedge f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\right)\to \left(\varnothing \ne \left\{\varnothing \right\}\wedge \varnothing \ne \left\{\left\{\varnothing \right\}\right\}\wedge \left\{\varnothing \right\}\ne \left\{\left\{\varnothing \right\}\right\}\right)$$
28		simpr	$$⊢\left(D\in V\wedge f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\right)\to f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D$$
29	23 27 28	f1dom3el3dif	$$⊢\left(D\in V\wedge f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\right)\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$
30	29	expcom	$$⊢f:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\to \left(D\in V\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\right)$$
31	30	exlimiv	$$⊢\exists ff:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\to \left(D\in V\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\right)$$
32	31	com12	$$⊢D\in V\to \left(\exists ff:\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\underset{1-1}{⟶}D\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\right)$$
33	22 32	sylbid	$$⊢D\in V\to \left(\left\{\varnothing ,\left\{\varnothing \right\},\left\{\left\{\varnothing \right\}\right\}\right\}\preccurlyeq D\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\right)$$
34	21 33	sylbid	$$⊢D\in V\to \left(3\le \left|D\right|\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\right)$$
35	34	imp	$$⊢\left(D\in V\wedge 3\le \left|D\right|\right)\to \exists x\in D\exists y\in D\exists z\in D\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$