This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )