Theorem gchinf

Description: An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015)

	Ref	Expression
Assertion	gchinf	|- ( ( A e. GCH /\ -. A e. Fin ) -> _om ~<_ A )

Proof

Step	Hyp	Ref	Expression
1		gchdju1	|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| 1o ) ~~ A )
2	1	ensymd	|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A |_| 1o ) )
3		isfin4-2	|- ( A e. GCH -> ( A e. Fin4 <-> -. _om ~<_ A ) )
4	3	adantr	|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A e. Fin4 <-> -. _om ~<_ A ) )
5		isfin4p1	|- ( A e. Fin4 <-> A ~< ( A |_| 1o ) )
6		sdomnen	|- ( A ~< ( A |_| 1o ) -> -. A ~~ ( A |_| 1o ) )
7	5 6	sylbi	|- ( A e. Fin4 -> -. A ~~ ( A |_| 1o ) )
8	4 7	biimtrrdi	|- ( ( A e. GCH /\ -. A e. Fin ) -> ( -. _om ~<_ A -> -. A ~~ ( A |_| 1o ) ) )
9	2 8	mt4d	|- ( ( A e. GCH /\ -. A e. Fin ) -> _om ~<_ A )