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 
|- S = { A , B }
Assertion hashprdifel 
|- ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )

Proof

Step Hyp Ref Expression
1 hashprdifel.s 
 |-  S = { A , B }
2 1 fveq2i 
 |-  ( # ` S ) = ( # ` { A , B } )
3 2 eqeq1i 
 |-  ( ( # ` S ) = 2 <-> ( # ` { A , B } ) = 2 )
4 hashprb 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) <-> ( # ` { A , B } ) = 2 )
5 3 4 bitr4i 
 |-  ( ( # ` S ) = 2 <-> ( A e. _V /\ B e. _V /\ A =/= B ) )
6 prid1g 
 |-  ( A e. _V -> A e. { A , B } )
7 6 3ad2ant1 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. { A , B } )
8 7 1 eleqtrrdi 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. S )
9 prid2g 
 |-  ( B e. _V -> B e. { A , B } )
10 9 3ad2ant2 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> B e. { A , B } )
11 10 1 eleqtrrdi 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> B e. S )
12 simp3 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A =/= B )
13 8 11 12 3jca 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> ( A e. S /\ B e. S /\ A =/= B ) )
14 5 13 sylbi 
 |-  ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )