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

Metamath Proof Explorer

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 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )