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 AVBWABAB=2

Proof

Step Hyp Ref Expression
1 simpr AVBWBW
2 elsni BAB=A
3 2 eqcomd BAA=B
4 3 necon3ai AB¬BA
5 snfi AFin
6 hashunsng BWAFin¬BAAB=A+1
7 6 imp BWAFin¬BAAB=A+1
8 5 7 mpanr1 BW¬BAAB=A+1
9 1 4 8 syl2an AVBWABAB=A+1
10 hashsng AVA=1
11 10 adantr AVBWA=1
12 11 adantr AVBWABA=1
13 12 oveq1d AVBWABA+1=1+1
14 9 13 eqtrd AVBWABAB=1+1
15 df-pr AB=AB
16 15 fveq2i AB=AB
17 df-2 2=1+1
18 14 16 17 3eqtr4g AVBWABAB=2
19 1ne2 12
20 19 a1i AVBW12
21 11 20 eqnetrd AVBWA2
22 dfsn2 A=AA
23 preq2 A=BAA=AB
24 22 23 eqtr2id A=BAB=A
25 24 fveq2d A=BAB=A
26 25 neeq1d A=BAB2A2
27 21 26 syl5ibrcom AVBWA=BAB2
28 27 necon2d AVBWAB=2AB
29 28 imp AVBWAB=2AB
30 18 29 impbida AVBWABAB=2