Theorem hashprdifel

Description: The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Hypothesis	hashprdifel.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
Assertion	hashprdifel	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		hashprdifel.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
2	1	fveq2i	⊢ ( ♯ ‘ 𝑆 ) = ( ♯ ‘ { 𝐴 , 𝐵 } )
3	2	eqeq1i	⊢ ( ( ♯ ‘ 𝑆 ) = 2 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
4		hashprb	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
5	3 4	bitr4i	⊢ ( ( ♯ ‘ 𝑆 ) = 2 ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) )
6		prid1g	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 , 𝐵 } )
7	6	3ad2ant1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
8	7 1	eleqtrrdi	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑆 )
9		prid2g	⊢ ( 𝐵 ∈ V → 𝐵 ∈ { 𝐴 , 𝐵 } )
10	9	3ad2ant2	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
11	10 1	eleqtrrdi	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑆 )
12		simp3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
13	8 11 12	3jca	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )
14	5 13	sylbi	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )