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 ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 ssfi ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → 𝐴 ∈ Fin )
2 1 3adant3 ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝐴 ∈ Fin )
3 hashen ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴𝐵 ) )
4 3 biimp3a ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝐴𝐵 )
5 pm3.2 ( 𝐵 ∈ Fin → ( 𝐴𝐵 → ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) ) )
6 5 3ad2ant2 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐴𝐵 → ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) ) )
7 fisseneq ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵𝐴𝐵 ) → 𝐴 = 𝐵 )
8 7 3expa ( ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) ∧ 𝐴𝐵 ) → 𝐴 = 𝐵 )
9 8 expcom ( 𝐴𝐵 → ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → 𝐴 = 𝐵 ) )
10 4 6 9 sylsyld ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐴𝐵𝐴 = 𝐵 ) )
11 10 3expb ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) ) → ( 𝐴𝐵𝐴 = 𝐵 ) )
12 11 expcom ( ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐴 ∈ Fin → ( 𝐴𝐵𝐴 = 𝐵 ) ) )
13 12 com23 ( ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐴𝐵 → ( 𝐴 ∈ Fin → 𝐴 = 𝐵 ) ) )
14 13 3impia ( ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ 𝐴𝐵 ) → ( 𝐴 ∈ Fin → 𝐴 = 𝐵 ) )
15 14 3com23 ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐴 ∈ Fin → 𝐴 = 𝐵 ) )
16 2 15 mpd ( ( 𝐵 ∈ Fin ∧ 𝐴𝐵 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝐴 = 𝐵 )