Theorem tpfi

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

	Ref	Expression
Assertion	tpfi	⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
3		snfi	⊢ { 𝐶 } ∈ Fin
4		unfi	⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ { 𝐶 } ∈ Fin ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∈ Fin )
5	2 3 4	mp2an	⊢ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∈ Fin
6	1 5	eqeltri	⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin