Description: Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb ). (Contributed by BTernaryTau, 9-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ensymfib | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bren | |
|
2 | 19.42v | |
|
3 | f1ocnv | |
|
4 | f1oenfirn | |
|
5 | 3 4 | sylan2 | |
6 | 5 | exlimiv | |
7 | 2 6 | sylbir | |
8 | 1 7 | sylan2b | |
9 | bren | |
|
10 | 19.42v | |
|
11 | f1ocnv | |
|
12 | f1oenfi | |
|
13 | 11 12 | sylan2 | |
14 | 13 | exlimiv | |
15 | 10 14 | sylbir | |
16 | 9 15 | sylan2b | |
17 | 8 16 | impbida | |