Metamath Proof Explorer


Theorem gchor

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

Ref Expression
Assertion gchor AGCH¬AFinABB𝒫AABB𝒫A

Proof

Step Hyp Ref Expression
1 simprr AGCH¬AFinABB𝒫AB𝒫A
2 brdom2 B𝒫AB𝒫AB𝒫A
3 1 2 sylib AGCH¬AFinABB𝒫AB𝒫AB𝒫A
4 gchen1 AGCH¬AFinABB𝒫AAB
5 4 expr AGCH¬AFinABB𝒫AAB
6 5 adantrr AGCH¬AFinABB𝒫AB𝒫AAB
7 6 orim1d AGCH¬AFinABB𝒫AB𝒫AB𝒫AABB𝒫A
8 3 7 mpd AGCH¬AFinABB𝒫AABB𝒫A