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 )