Metamath Proof Explorer

Theorem tpfi

Description: An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013)

Ref Expression
Assertion tpfi 
|- { A , B , C } e. Fin

Proof

Step Hyp Ref Expression
1 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
2 prfi 
 |-  { A , B } e. Fin
3 snfi 
 |-  { C } e. Fin
4 unfi 
 |-  ( ( { A , B } e. Fin /\ { C } e. Fin ) -> ( { A , B } u. { C } ) e. Fin )
5 2 3 4 mp2an 
 |-  ( { A , B } u. { C } ) e. Fin
6 1 5 eqeltri 
 |-  { A , B , C } e. Fin