Metamath Proof Explorer


Theorem finngch

Description: The exclusion of finite sets from consideration in df-gch is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015)

Ref Expression
Assertion finngch AFin1𝑜AAA⊔︀1𝑜A⊔︀1𝑜𝒫A

Proof

Step Hyp Ref Expression
1 fin12 AFinAFinII
2 fin23 AFinIIAFinIII
3 fin34 AFinIIIAFinIV
4 1 2 3 3syl AFinAFinIV
5 isfin4p1 AFinIVAA⊔︀1𝑜
6 4 5 sylib AFinAA⊔︀1𝑜
7 canthp1 1𝑜AA⊔︀1𝑜𝒫A
8 6 7 anim12i AFin1𝑜AAA⊔︀1𝑜A⊔︀1𝑜𝒫A