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 } e. Fin /\ ( # ` { A , B , C } ) <_ 3 )

Proof

Step Hyp Ref Expression
1 df-tp
 |-  { A , B , C } = ( { A , B } u. { C } )
2 hashprlei
 |-  ( { A , B } e. Fin /\ ( # ` { A , B } ) <_ 2 )
3 hashsnlei
 |-  ( { C } e. Fin /\ ( # ` { C } ) <_ 1 )
4 2nn0
 |-  2 e. NN0
5 1nn0
 |-  1 e. NN0
6 2p1e3
 |-  ( 2 + 1 ) = 3
7 1 2 3 4 5 6 hashunlei
 |-  ( { A , B , C } e. Fin /\ ( # ` { A , B , C } ) <_ 3 )