Metamath Proof Explorer


Theorem gchinf

Description: An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchinf AGCH¬AFinωA

Proof

Step Hyp Ref Expression
1 gchdju1 AGCH¬AFinA⊔︀1𝑜A
2 1 ensymd AGCH¬AFinAA⊔︀1𝑜
3 isfin4-2 AGCHAFinIV¬ωA
4 3 adantr AGCH¬AFinAFinIV¬ωA
5 isfin4p1 AFinIVAA⊔︀1𝑜
6 sdomnen AA⊔︀1𝑜¬AA⊔︀1𝑜
7 5 6 sylbi AFinIV¬AA⊔︀1𝑜
8 4 7 syl6bir AGCH¬AFin¬ωA¬AA⊔︀1𝑜
9 2 8 mt4d AGCH¬AFinωA