Theorem gchen2

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

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

Proof

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