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∈Fin∧A⊆B∧A=B→A=B

Proof

Step Hyp Ref Expression
1 ssfi ⊢B∈Fin∧A⊆B→A∈Fin
2 1 3adant3 ⊢B∈Fin∧A⊆B∧A=B→A∈Fin
3 hashen ⊢A∈Fin∧B∈Fin→A=B↔A≈B
4 3 biimp3a ⊢A∈Fin∧B∈Fin∧A=B→A≈B
5 pm3.2 ⊢B∈Fin→A⊆B→B∈Fin∧A⊆B
6 5 3ad2ant2 ⊢A∈Fin∧B∈Fin∧A=B→A⊆B→B∈Fin∧A⊆B
7 fisseneq ⊢B∈Fin∧A⊆B∧A≈B→A=B
8 7 3expa ⊢B∈Fin∧A⊆B∧A≈B→A=B
9 8 expcom ⊢A≈B→B∈Fin∧A⊆B→A=B
10 4 6 9 sylsyld ⊢A∈Fin∧B∈Fin∧A=B→A⊆B→A=B
11 10 3expb ⊢A∈Fin∧B∈Fin∧A=B→A⊆B→A=B
12 11 expcom ⊢B∈Fin∧A=B→A∈Fin→A⊆B→A=B
13 12 com23 ⊢B∈Fin∧A=B→A⊆B→A∈Fin→A=B
14 13 3impia ⊢B∈Fin∧A=B∧A⊆B→A∈Fin→A=B
15 14 3com23 ⊢B∈Fin∧A⊆B∧A=B→A∈Fin→A=B
16 2 15 mpd ⊢B∈Fin∧A⊆B∧A=B→A=B