Theorem gchen1

Description: If A <_ B < ~P A , and A is an infinite GCH-set, then A = B in cardinality. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	gchen1	|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~< ~P A ) ) -> A ~~ B )

Proof

Step	Hyp	Ref	Expression
1		simprl	|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~< ~P A ) ) -> A ~<_ B )
2		gchi	|- ( ( A e. GCH /\ A ~< B /\ B ~< ~P A ) -> A e. Fin )
3	2	3com23	|- ( ( A e. GCH /\ B ~< ~P A /\ A ~< B ) -> A e. Fin )
4	3	3expia	|- ( ( A e. GCH /\ B ~< ~P A ) -> ( A ~< B -> A e. Fin ) )
5	4	con3dimp	|- ( ( ( A e. GCH /\ B ~< ~P A ) /\ -. A e. Fin ) -> -. A ~< B )
6	5	an32s	|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ B ~< ~P A ) -> -. A ~< B )
7	6	adantrl	|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~< ~P A ) ) -> -. A ~< B )
8		bren2	|- ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )
9	1 7 8	sylanbrc	|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~< ~P A ) ) -> A ~~ B )