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	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		0nep0	⊢ ∅ ≠ { ∅ }
2		0ex	⊢ ∅ ∈ V
3	2	sneqr	⊢ ( { ∅ } = { { ∅ } } → ∅ = { ∅ } )
4	3	necon3i	⊢ ( ∅ ≠ { ∅ } → { ∅ } ≠ { { ∅ } } )
5	1 4	ax-mp	⊢ { ∅ } ≠ { { ∅ } }
6		snex	⊢ { ∅ } ∈ V
7		snnzg	⊢ ( { ∅ } ∈ V → { { ∅ } } ≠ ∅ )
8	6 7	ax-mp	⊢ { { ∅ } } ≠ ∅
9	1 5 8	3pm3.2i	⊢ ( ∅ ≠ { ∅ } ∧ { ∅ } ≠ { { ∅ } } ∧ { { ∅ } } ≠ ∅ )
10		snex	⊢ { { ∅ } } ∈ V
11	2 6 10	3pm3.2i	⊢ ( ∅ ∈ V ∧ { ∅ } ∈ V ∧ { { ∅ } } ∈ V )
12		hashtpg	⊢ ( ( ∅ ∈ V ∧ { ∅ } ∈ V ∧ { { ∅ } } ∈ V ) → ( ( ∅ ≠ { ∅ } ∧ { ∅ } ≠ { { ∅ } } ∧ { { ∅ } } ≠ ∅ ) ↔ ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) = 3 ) )
13	11 12	ax-mp	⊢ ( ( ∅ ≠ { ∅ } ∧ { ∅ } ≠ { { ∅ } } ∧ { { ∅ } } ≠ ∅ ) ↔ ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) = 3 )
14	9 13	mpbi	⊢ ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) = 3
15	14	eqcomi	⊢ 3 = ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } )
16	15	a1i	⊢ ( 𝐷 ∈ 𝑉 → 3 = ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) )
17	16	breq1d	⊢ ( 𝐷 ∈ 𝑉 → ( 3 ≤ ( ♯ ‘ 𝐷 ) ↔ ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) ≤ ( ♯ ‘ 𝐷 ) ) )
18		tpfi	⊢ { ∅ , { ∅ } , { { ∅ } } } ∈ Fin
19		hashdom	⊢ ( ( { ∅ , { ∅ } , { { ∅ } } } ∈ Fin ∧ 𝐷 ∈ 𝑉 ) → ( ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) ≤ ( ♯ ‘ 𝐷 ) ↔ { ∅ , { ∅ } , { { ∅ } } } ≼ 𝐷 ) )
20	18 19	mpan	⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ { ∅ , { ∅ } , { { ∅ } } } ) ≤ ( ♯ ‘ 𝐷 ) ↔ { ∅ , { ∅ } , { { ∅ } } } ≼ 𝐷 ) )
21	17 20	bitrd	⊢ ( 𝐷 ∈ 𝑉 → ( 3 ≤ ( ♯ ‘ 𝐷 ) ↔ { ∅ , { ∅ } , { { ∅ } } } ≼ 𝐷 ) )
22		brdomg	⊢ ( 𝐷 ∈ 𝑉 → ( { ∅ , { ∅ } , { { ∅ } } } ≼ 𝐷 ↔ ∃ 𝑓 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 ) )
23	11	a1i	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 ) → ( ∅ ∈ V ∧ { ∅ } ∈ V ∧ { { ∅ } } ∈ V ) )
24	7	necomd	⊢ ( { ∅ } ∈ V → ∅ ≠ { { ∅ } } )
25	6 24	ax-mp	⊢ ∅ ≠ { { ∅ } }
26	1 25 5	3pm3.2i	⊢ ( ∅ ≠ { ∅ } ∧ ∅ ≠ { { ∅ } } ∧ { ∅ } ≠ { { ∅ } } )
27	26	a1i	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 ) → ( ∅ ≠ { ∅ } ∧ ∅ ≠ { { ∅ } } ∧ { ∅ } ≠ { { ∅ } } ) )
28		simpr	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 ) → 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 )
29	23 27 28	f1dom3el3dif	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) )
30	29	expcom	⊢ ( 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 → ( 𝐷 ∈ 𝑉 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) )
31	30	exlimiv	⊢ ( ∃ 𝑓 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 → ( 𝐷 ∈ 𝑉 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) )
32	31	com12	⊢ ( 𝐷 ∈ 𝑉 → ( ∃ 𝑓 𝑓 : { ∅ , { ∅ } , { { ∅ } } } –1-1→ 𝐷 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) )
33	22 32	sylbid	⊢ ( 𝐷 ∈ 𝑉 → ( { ∅ , { ∅ } , { { ∅ } } } ≼ 𝐷 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) )
34	21 33	sylbid	⊢ ( 𝐷 ∈ 𝑉 → ( 3 ≤ ( ♯ ‘ 𝐷 ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) )
35	34	imp	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) )