Metamath Proof Explorer

Theorem hashtplei

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

Ref Expression
Assertion hashtplei ⊢ A B C ∈ Fin ∧ A B C ≤ 3

Proof

Step Hyp Ref Expression
1 df-tp ⊢ A B C = A B ∪ C
2 hashprlei ⊢ A B ∈ Fin ∧ A B ≤ 2
3 hashsnlei ⊢ C ∈ Fin ∧ C ≤ 1
4 2nn0 ⊢ 2 ∈ ℕ 0
5 1nn0 ⊢ 1 ∈ ℕ 0
6 2p1e3 ⊢ 2 + 1 = 3
7 1 2 3 4 5 6 hashunlei ⊢ A B C ∈ Fin ∧ A B C ≤ 3