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 ) )