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 syl5req 
 |-  ( 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 ) )