Metamath Proof Explorer

Theorem fisshasheq

Description: A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023)

Ref Expression
Assertion fisshasheq 
|- ( ( B e. Fin /\ A C_ B /\ ( # ` A ) = ( # ` B ) ) -> A = B )

Proof

Step Hyp Ref Expression
1 ssfi 
 |-  ( ( B e. Fin /\ A C_ B ) -> A e. Fin )
2 1 3adant3 
 |-  ( ( B e. Fin /\ A C_ B /\ ( # ` A ) = ( # ` B ) ) -> A e. Fin )
3 hashen 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
4 3 biimp3a 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( # ` A ) = ( # ` B ) ) -> A ~~ B )
5 pm3.2 
 |-  ( B e. Fin -> ( A C_ B -> ( B e. Fin /\ A C_ B ) ) )
6 5 3ad2ant2 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( # ` A ) = ( # ` B ) ) -> ( A C_ B -> ( B e. Fin /\ A C_ B ) ) )
7 fisseneq 
 |-  ( ( B e. Fin /\ A C_ B /\ A ~~ B ) -> A = B )
8 7 3expa 
 |-  ( ( ( B e. Fin /\ A C_ B ) /\ A ~~ B ) -> A = B )
9 8 expcom 
 |-  ( A ~~ B -> ( ( B e. Fin /\ A C_ B ) -> A = B ) )
10 4 6 9 sylsyld 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( # ` A ) = ( # ` B ) ) -> ( A C_ B -> A = B ) )
11 10 3expb 
 |-  ( ( A e. Fin /\ ( B e. Fin /\ ( # ` A ) = ( # ` B ) ) ) -> ( A C_ B -> A = B ) )
12 11 expcom 
 |-  ( ( B e. Fin /\ ( # ` A ) = ( # ` B ) ) -> ( A e. Fin -> ( A C_ B -> A = B ) ) )
13 12 com23 
 |-  ( ( B e. Fin /\ ( # ` A ) = ( # ` B ) ) -> ( A C_ B -> ( A e. Fin -> A = B ) ) )
14 13 3impia 
 |-  ( ( B e. Fin /\ ( # ` A ) = ( # ` B ) /\ A C_ B ) -> ( A e. Fin -> A = B ) )
15 14 3com23 
 |-  ( ( B e. Fin /\ A C_ B /\ ( # ` A ) = ( # ` B ) ) -> ( A e. Fin -> A = B ) )
16 2 15 mpd 
 |-  ( ( B e. Fin /\ A C_ B /\ ( # ` A ) = ( # ` B ) ) -> A = B )