Metamath Proof Explorer

Theorem ctbnfien

Description: An infinite subset of a countable set is countable, without using choice. (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

		Ref	Expression
	Assertion	ctbnfien	$⊢ ((X \approx ω \land Y \approx ω) \land (A \subseteq X \land \neg A \in Fin)) \to A \approx Y$

Proof

Step	Hyp	Ref	Expression
1		isfinite	$⊢ A \in Fin \leftrightarrow A ≺ ω$
2	1	notbii	$⊢ \neg A \in Fin \leftrightarrow \neg A ≺ ω$
3		relen	$⊢ Rel \approx$
4	3	brrelex1i	$⊢ X \approx ω \to X \in V$
5		ssdomg	$⊢ X \in V \to (A \subseteq X \to A ≼ X)$
6	4 5	syl	$⊢ X \approx ω \to (A \subseteq X \to A ≼ X)$
7		domen2	$⊢ X \approx ω \to (A ≼ X \leftrightarrow A ≼ ω)$
8	6 7	sylibd	$⊢ X \approx ω \to (A \subseteq X \to A ≼ ω)$
9	8	imp	$⊢ (X \approx ω \land A \subseteq X) \to A ≼ ω$
10		brdom2	$⊢ A ≼ ω \leftrightarrow (A ≺ ω \lor A \approx ω)$
11	9 10	sylib	$⊢ (X \approx ω \land A \subseteq X) \to (A ≺ ω \lor A \approx ω)$
12	11	adantlr	$⊢ ((X \approx ω \land Y \approx ω) \land A \subseteq X) \to (A ≺ ω \lor A \approx ω)$
13	12	ord	$⊢ ((X \approx ω \land Y \approx ω) \land A \subseteq X) \to (\neg A ≺ ω \to A \approx ω)$
14	2 13	biimtrid	$⊢ ((X \approx ω \land Y \approx ω) \land A \subseteq X) \to (\neg A \in Fin \to A \approx ω)$
15	14	impr	$⊢ ((X \approx ω \land Y \approx ω) \land (A \subseteq X \land \neg A \in Fin)) \to A \approx ω$
16		enen2	$⊢ Y \approx ω \to (A \approx Y \leftrightarrow A \approx ω)$
17	16	ad2antlr	$⊢ ((X \approx ω \land Y \approx ω) \land (A \subseteq X \land \neg A \in Fin)) \to (A \approx Y \leftrightarrow A \approx ω)$
18	15 17	mpbird	$⊢ ((X \approx ω \land Y \approx ω) \land (A \subseteq X \land \neg A \in Fin)) \to A \approx Y$