Metamath Proof Explorer


Theorem ensymfib

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 AFinABBA

Proof

Step Hyp Ref Expression
1 bren ABff:A1-1 ontoB
2 19.42v fAFinf:A1-1 ontoBAFinff:A1-1 ontoB
3 f1ocnv f:A1-1 ontoBf-1:B1-1 ontoA
4 f1oenfirn AFinf-1:B1-1 ontoABA
5 3 4 sylan2 AFinf:A1-1 ontoBBA
6 5 exlimiv fAFinf:A1-1 ontoBBA
7 2 6 sylbir AFinff:A1-1 ontoBBA
8 1 7 sylan2b AFinABBA
9 bren BAgg:B1-1 ontoA
10 19.42v gAFing:B1-1 ontoAAFingg:B1-1 ontoA
11 f1ocnv g:B1-1 ontoAg-1:A1-1 ontoB
12 f1oenfi AFing-1:A1-1 ontoBAB
13 11 12 sylan2 AFing:B1-1 ontoAAB
14 13 exlimiv gAFing:B1-1 ontoAAB
15 10 14 sylbir AFingg:B1-1 ontoAAB
16 9 15 sylan2b AFinBAAB
17 8 16 impbida AFinABBA