Theorem fisseneq

Description: A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008)

	Ref	Expression
Assertion	fisseneq	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-pss	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
2		pssinf	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ∈ Fin )
3	2	expcom	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ⊊ 𝐵 → ¬ 𝐵 ∈ Fin ) )
4	1 3	biimtrrid	⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ¬ 𝐵 ∈ Fin ) )
5	4	expdimp	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ Fin ) )
6	5	necon4ad	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∈ Fin → 𝐴 = 𝐵 ) )
7	6	3impia	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 = 𝐵 )
8	7	3com13	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → 𝐴 = 𝐵 )