Metamath Proof Explorer

Theorem hasheqf1o

Description: The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017)

		Ref	Expression
	Assertion	hasheqf1o	\|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> E. f f : A -1-1-onto-> B ) )

Proof

Step	Hyp	Ref	Expression
1		hashen	\|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
2		bren	\|- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
3	1 2	bitrdi	\|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> E. f f : A -1-1-onto-> B ) )

Step

Hyp

Ref

Expression

hashen

 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )

bren

 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )

1 2

bitrdi

 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> E. f f : A -1-1-onto-> B ) )