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 )