Theorem prfi

Description: An unordered pair is finite. (Contributed by NM, 22-Aug-2008)

	Ref	Expression
Assertion	prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin

Proof

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