This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ Fin

Proof

Step Hyp Ref Expression
1 df-tp ⊢ A B C = A B ∪ C
2 prfi ⊢ A B ∈ Fin
3 snfi ⊢ C ∈ Fin
4 unfi ⊢ A B ∈ Fin ∧ C ∈ Fin → A B ∪ C ∈ Fin
5 2 3 4 mp2an ⊢ A B ∪ C ∈ Fin
6 1 5 eqeltri ⊢ A B C ∈ Fin