Metamath Proof Explorer


Theorem hashprg

Description: The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013) (Revised by Mario Carneiro, 5-May-2016) (Revised by AV, 18-Sep-2021)

Ref Expression
Assertion hashprg
|- ( ( A e. V /\ B e. W ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
2 elsni
 |-  ( B e. { A } -> B = A )
3 2 eqcomd
 |-  ( B e. { A } -> A = B )
4 3 necon3ai
 |-  ( A =/= B -> -. B e. { A } )
5 snfi
 |-  { A } e. Fin
6 hashunsng
 |-  ( B e. W -> ( ( { A } e. Fin /\ -. B e. { A } ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) ) )
7 6 imp
 |-  ( ( B e. W /\ ( { A } e. Fin /\ -. B e. { A } ) ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) )
8 5 7 mpanr1
 |-  ( ( B e. W /\ -. B e. { A } ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) )
9 1 4 8 syl2an
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) )
10 hashsng
 |-  ( A e. V -> ( # ` { A } ) = 1 )
11 10 adantr
 |-  ( ( A e. V /\ B e. W ) -> ( # ` { A } ) = 1 )
12 11 adantr
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` { A } ) = 1 )
13 12 oveq1d
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( ( # ` { A } ) + 1 ) = ( 1 + 1 ) )
14 9 13 eqtrd
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` ( { A } u. { B } ) ) = ( 1 + 1 ) )
15 df-pr
 |-  { A , B } = ( { A } u. { B } )
16 15 fveq2i
 |-  ( # ` { A , B } ) = ( # ` ( { A } u. { B } ) )
17 df-2
 |-  2 = ( 1 + 1 )
18 14 16 17 3eqtr4g
 |-  ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
19 1ne2
 |-  1 =/= 2
20 19 a1i
 |-  ( ( A e. V /\ B e. W ) -> 1 =/= 2 )
21 11 20 eqnetrd
 |-  ( ( A e. V /\ B e. W ) -> ( # ` { A } ) =/= 2 )
22 dfsn2
 |-  { A } = { A , A }
23 preq2
 |-  ( A = B -> { A , A } = { A , B } )
24 22 23 eqtr2id
 |-  ( A = B -> { A , B } = { A } )
25 24 fveq2d
 |-  ( A = B -> ( # ` { A , B } ) = ( # ` { A } ) )
26 25 neeq1d
 |-  ( A = B -> ( ( # ` { A , B } ) =/= 2 <-> ( # ` { A } ) =/= 2 ) )
27 21 26 syl5ibrcom
 |-  ( ( A e. V /\ B e. W ) -> ( A = B -> ( # ` { A , B } ) =/= 2 ) )
28 27 necon2d
 |-  ( ( A e. V /\ B e. W ) -> ( ( # ` { A , B } ) = 2 -> A =/= B ) )
29 28 imp
 |-  ( ( ( A e. V /\ B e. W ) /\ ( # ` { A , B } ) = 2 ) -> A =/= B )
30 18 29 impbida
 |-  ( ( A e. V /\ B e. W ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )