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	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ) → 𝐴 ≈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		isfinite	⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω )
2	1	notbii	⊢ ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ≺ ω )
3		relen	⊢ Rel ≈
4	3	brrelex1i	⊢ ( 𝑋 ≈ ω → 𝑋 ∈ V )
5		ssdomg	⊢ ( 𝑋 ∈ V → ( 𝐴 ⊆ 𝑋 → 𝐴 ≼ 𝑋 ) )
6	4 5	syl	⊢ ( 𝑋 ≈ ω → ( 𝐴 ⊆ 𝑋 → 𝐴 ≼ 𝑋 ) )
7		domen2	⊢ ( 𝑋 ≈ ω → ( 𝐴 ≼ 𝑋 ↔ 𝐴 ≼ ω ) )
8	6 7	sylibd	⊢ ( 𝑋 ≈ ω → ( 𝐴 ⊆ 𝑋 → 𝐴 ≼ ω ) )
9	8	imp	⊢ ( ( 𝑋 ≈ ω ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ≼ ω )
10		brdom2	⊢ ( 𝐴 ≼ ω ↔ ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) )
11	9 10	sylib	⊢ ( ( 𝑋 ≈ ω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) )
12	11	adantlr	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) )
13	12	ord	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ 𝐴 ⊆ 𝑋 ) → ( ¬ 𝐴 ≺ ω → 𝐴 ≈ ω ) )
14	2 13	biimtrid	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ 𝐴 ⊆ 𝑋 ) → ( ¬ 𝐴 ∈ Fin → 𝐴 ≈ ω ) )
15	14	impr	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ) → 𝐴 ≈ ω )
16		enen2	⊢ ( 𝑌 ≈ ω → ( 𝐴 ≈ 𝑌 ↔ 𝐴 ≈ ω ) )
17	16	ad2antlr	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ) → ( 𝐴 ≈ 𝑌 ↔ 𝐴 ≈ ω ) )
18	15 17	mpbird	⊢ ( ( ( 𝑋 ≈ ω ∧ 𝑌 ≈ ω ) ∧ ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ) → 𝐴 ≈ 𝑌 )