Metamath Proof Explorer

Theorem hashprlei

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

Ref Expression
Assertion hashprlei 
|- ( { A , B } e. Fin /\ ( # ` { A , B } ) <_ 2 )

Proof

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