fisseneq

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

		Ref	Expression
	Assertion	fisseneq	$⊢ (B \in Fin \land A \subseteq B \land A \approx B) \to A = B$

Step	Hyp	Ref	Expression
1		df-pss	$⊢ A \subset B \leftrightarrow (A \subseteq B \land A \neq B)$
2		pssinf	$⊢ (A \subset B \land A \approx B) \to \neg B \in Fin$
3	2	expcom	$⊢ A \approx B \to (A \subset B \to \neg B \in Fin)$
4	1 3	biimtrrid	$⊢ A \approx B \to ((A \subseteq B \land A \neq B) \to \neg B \in Fin)$
5	4	expdimp	$⊢ (A \approx B \land A \subseteq B) \to (A \neq B \to \neg B \in Fin)$
6	5	necon4ad	$⊢ (A \approx B \land A \subseteq B) \to (B \in Fin \to A = B)$
7	6	3impia	$⊢ (A \approx B \land A \subseteq B \land B \in Fin) \to A = B$
8	7	3com13	$⊢ (B \in Fin \land A \subseteq B \land A \approx B) \to A = B$

Metamath Proof Explorer