Theorem hashprlei

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

	Ref	Expression
Assertion	hashprlei	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ 2 )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		hashsnlei	⊢ ( { 𝐴 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 } ) ≤ 1 )
3		hashsnlei	⊢ ( { 𝐵 } ∈ Fin ∧ ( ♯ ‘ { 𝐵 } ) ≤ 1 )
4		1nn0	⊢ 1 ∈ ℕ0
5		1p1e2	⊢ ( 1 + 1 ) = 2
6	1 2 3 4 4 5	hashunlei	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ 2 )