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 ~~ _om /\ Y ~~ _om ) /\ ( A C_ X /\ -. A e. Fin ) ) -> A ~~ Y )

Proof

Step	Hyp	Ref	Expression
1		isfinite	|- ( A e. Fin <-> A ~< _om )
2	1	notbii	|- ( -. A e. Fin <-> -. A ~< _om )
3		relen	|- Rel ~~
4	3	brrelex1i	|- ( X ~~ _om -> X e. _V )
5		ssdomg	|- ( X e. _V -> ( A C_ X -> A ~<_ X ) )
6	4 5	syl	|- ( X ~~ _om -> ( A C_ X -> A ~<_ X ) )
7		domen2	|- ( X ~~ _om -> ( A ~<_ X <-> A ~<_ _om ) )
8	6 7	sylibd	|- ( X ~~ _om -> ( A C_ X -> A ~<_ _om ) )
9	8	imp	|- ( ( X ~~ _om /\ A C_ X ) -> A ~<_ _om )
10		brdom2	|- ( A ~<_ _om <-> ( A ~< _om \/ A ~~ _om ) )
11	9 10	sylib	|- ( ( X ~~ _om /\ A C_ X ) -> ( A ~< _om \/ A ~~ _om ) )
12	11	adantlr	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ A C_ X ) -> ( A ~< _om \/ A ~~ _om ) )
13	12	ord	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ A C_ X ) -> ( -. A ~< _om -> A ~~ _om ) )
14	2 13	biimtrid	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ A C_ X ) -> ( -. A e. Fin -> A ~~ _om ) )
15	14	impr	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ ( A C_ X /\ -. A e. Fin ) ) -> A ~~ _om )
16		enen2	|- ( Y ~~ _om -> ( A ~~ Y <-> A ~~ _om ) )
17	16	ad2antlr	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ ( A C_ X /\ -. A e. Fin ) ) -> ( A ~~ Y <-> A ~~ _om ) )
18	15 17	mpbird	|- ( ( ( X ~~ _om /\ Y ~~ _om ) /\ ( A C_ X /\ -. A e. Fin ) ) -> A ~~ Y )