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

Metamath Proof Explorer

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 )