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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | elsni | |
|
3 | 2 | eqcomd | |
4 | 3 | necon3ai | |
5 | snfi | |
|
6 | hashunsng | |
|
7 | 6 | imp | |
8 | 5 7 | mpanr1 | |
9 | 1 4 8 | syl2an | |
10 | hashsng | |
|
11 | 10 | adantr | |
12 | 11 | adantr | |
13 | 12 | oveq1d | |
14 | 9 13 | eqtrd | |
15 | df-pr | |
|
16 | 15 | fveq2i | |
17 | df-2 | |
|
18 | 14 16 17 | 3eqtr4g | |
19 | 1ne2 | |
|
20 | 19 | a1i | |
21 | 11 20 | eqnetrd | |
22 | dfsn2 | |
|
23 | preq2 | |
|
24 | 22 23 | eqtr2id | |
25 | 24 | fveq2d | |
26 | 25 | neeq1d | |
27 | 21 26 | syl5ibrcom | |
28 | 27 | necon2d | |
29 | 28 | imp | |
30 | 18 29 | impbida | |