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