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

Metamath Proof Explorer

Theorem gchdju1

Description: An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion gchdju1 
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| 1o ) ~~ A )

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 1 a1i 
 |-  ( -. A e. Fin -> 1o e. _om )
3 djudoml 
 |-  ( ( A e. GCH /\ 1o e. _om ) -> A ~<_ ( A |_| 1o ) )
4 2 3 sylan2 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ( A |_| 1o ) )
5 simpr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> -. A e. Fin )
6 nnfi 
 |-  ( 1o e. _om -> 1o e. Fin )
7 1 6 mp1i 
 |-  ( -. A e. Fin -> 1o e. Fin )
8 fidomtri2 
 |-  ( ( A e. GCH /\ 1o e. Fin ) -> ( A ~<_ 1o <-> -. 1o ~< A ) )
9 7 8 sylan2 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ 1o <-> -. 1o ~< A ) )
10 1 6 mp1i 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> 1o e. Fin )
11 domfi 
 |-  ( ( 1o e. Fin /\ A ~<_ 1o ) -> A e. Fin )
12 11 ex 
 |-  ( 1o e. Fin -> ( A ~<_ 1o -> A e. Fin ) )
13 10 12 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ 1o -> A e. Fin ) )
14 9 13 sylbird 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( -. 1o ~< A -> A e. Fin ) )
15 5 14 mt3d 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> 1o ~< A )
16 canthp1 
 |-  ( 1o ~< A -> ( A |_| 1o ) ~< ~P A )
17 15 16 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| 1o ) ~< ~P A )
18 4 17 jca 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ ( A |_| 1o ) /\ ( A |_| 1o ) ~< ~P A ) )
19 gchen1 
 |-  ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ ( A |_| 1o ) /\ ( A |_| 1o ) ~< ~P A ) ) -> A ~~ ( A |_| 1o ) )
20 18 19 mpdan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A |_| 1o ) )
21 20 ensymd 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| 1o ) ~~ A )