Theorem hashtplei

Description: An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	hashtplei	⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) ≤ 3 )

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2		hashprlei	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ 2 )
3		hashsnlei	⊢ ( { 𝐶 } ∈ Fin ∧ ( ♯ ‘ { 𝐶 } ) ≤ 1 )
4		2nn0	⊢ 2 ∈ ℕ0
5		1nn0	⊢ 1 ∈ ℕ0
6		2p1e3	⊢ ( 2 + 1 ) = 3
7	1 2 3 4 5 6	hashunlei	⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) ≤ 3 )