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 V B W A B A B = 2

Proof

Step Hyp Ref Expression
1 simpr A V B W B W
2 elsni B A B = A
3 2 eqcomd B A A = B
4 3 necon3ai A B ¬ B A
5 snfi A Fin
6 hashunsng B W A Fin ¬ B A A B = A + 1
7 6 imp B W A Fin ¬ B A A B = A + 1
8 5 7 mpanr1 B W ¬ B A A B = A + 1
9 1 4 8 syl2an A V B W A B A B = A + 1
10 hashsng A V A = 1
11 10 adantr A V B W A = 1
12 11 adantr A V B W A B A = 1
13 12 oveq1d A V B W A B A + 1 = 1 + 1
14 9 13 eqtrd A V B W A B A B = 1 + 1
15 df-pr A B = A B
16 15 fveq2i A B = A B
17 df-2 2 = 1 + 1
18 14 16 17 3eqtr4g A V B W A B A B = 2
19 1ne2 1 2
20 19 a1i A V B W 1 2
21 11 20 eqnetrd A V B 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 V B W A = B A B 2
28 27 necon2d A V B W A B = 2 A B
29 28 imp A V B W A B = 2 A B
30 18 29 impbida A V B W A B A B = 2