Metamath Proof Explorer

Theorem infpss

Description: Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of TakeutiZaring p. 91. See also infpssALT . (Contributed by NM, 23-Oct-2004) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	infpss	$⊢ ω ≼ A \to \exists x (x \subset A \land x \approx A)$

Proof

Step	Hyp	Ref	Expression
1		infn0	$⊢ ω ≼ A \to A \neq \emptyset$
2		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
3	1 2	sylib	$⊢ ω ≼ A \to \exists y y \in A$
4		reldom	$⊢ Rel ≼$
5	4	brrelex2i	$⊢ ω ≼ A \to A \in V$
6		difexg	$⊢ A \in V \to A ∖ \{y\} \in V$
7	5 6	syl	$⊢ ω ≼ A \to A ∖ \{y\} \in V$
8	7	adantr	$⊢ (ω ≼ A \land y \in A) \to A ∖ \{y\} \in V$
9		simpr	$⊢ (ω ≼ A \land y \in A) \to y \in A$
10		difsnpss	$⊢ y \in A \leftrightarrow A ∖ \{y\} \subset A$
11	9 10	sylib	$⊢ (ω ≼ A \land y \in A) \to A ∖ \{y\} \subset A$
12		infdifsn	$⊢ ω ≼ A \to (A ∖ \{y\}) \approx A$
13	12	adantr	$⊢ (ω ≼ A \land y \in A) \to (A ∖ \{y\}) \approx A$
14	11 13	jca	$⊢ (ω ≼ A \land y \in A) \to (A ∖ \{y\} \subset A \land (A ∖ \{y\}) \approx A)$
15		psseq1	$⊢ x = A ∖ \{y\} \to (x \subset A \leftrightarrow A ∖ \{y\} \subset A)$
16		breq1	$⊢ x = A ∖ \{y\} \to (x \approx A \leftrightarrow (A ∖ \{y\}) \approx A)$
17	15 16	anbi12d	$⊢ x = A ∖ \{y\} \to ((x \subset A \land x \approx A) \leftrightarrow (A ∖ \{y\} \subset A \land (A ∖ \{y\}) \approx A))$
18	8 14 17	spcedv	$⊢ (ω ≼ A \land y \in A) \to \exists x (x \subset A \land x \approx A)$
19	3 18	exlimddv	$⊢ ω ≼ A \to \exists x (x \subset A \land x \approx A)$