This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A e. Fin -> ( A ~~ B <-> B ~~ A ) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 19.42v 
 |-  ( E. f ( A e. Fin /\ f : A -1-1-onto-> B ) <-> ( A e. Fin /\ E. f f : A -1-1-onto-> B ) )
3 f1ocnv 
 |-  ( f : A -1-1-onto-> B -> `' f : B -1-1-onto-> A )
4 f1oenfirn 
 |-  ( ( A e. Fin /\ `' f : B -1-1-onto-> A ) -> B ~~ A )
5 3 4 sylan2 
 |-  ( ( A e. Fin /\ f : A -1-1-onto-> B ) -> B ~~ A )
6 5 exlimiv 
 |-  ( E. f ( A e. Fin /\ f : A -1-1-onto-> B ) -> B ~~ A )
7 2 6 sylbir 
 |-  ( ( A e. Fin /\ E. f f : A -1-1-onto-> B ) -> B ~~ A )
8 1 7 sylan2b 
 |-  ( ( A e. Fin /\ A ~~ B ) -> B ~~ A )
9 bren 
 |-  ( B ~~ A <-> E. g g : B -1-1-onto-> A )
10 19.42v 
 |-  ( E. g ( A e. Fin /\ g : B -1-1-onto-> A ) <-> ( A e. Fin /\ E. g g : B -1-1-onto-> A ) )
11 f1ocnv 
 |-  ( g : B -1-1-onto-> A -> `' g : A -1-1-onto-> B )
12 f1oenfi 
 |-  ( ( A e. Fin /\ `' g : A -1-1-onto-> B ) -> A ~~ B )
13 11 12 sylan2 
 |-  ( ( A e. Fin /\ g : B -1-1-onto-> A ) -> A ~~ B )
14 13 exlimiv 
 |-  ( E. g ( A e. Fin /\ g : B -1-1-onto-> A ) -> A ~~ B )
15 10 14 sylbir 
 |-  ( ( A e. Fin /\ E. g g : B -1-1-onto-> A ) -> A ~~ B )
16 9 15 sylan2b 
 |-  ( ( A e. Fin /\ B ~~ A ) -> A ~~ B )
17 8 16 impbida 
 |-  ( A e. Fin -> ( A ~~ B <-> B ~~ A ) )