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	$$⊢\left(A\in \mathrm{Fin}\wedge 1_{𝑜}\prec A\right)\to \left(A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\wedge \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fin12	$$⊢A\in \mathrm{Fin}\to A\in {\mathrm{Fin}}^{\mathrm{II}}$$
2		fin23	$$⊢A\in {\mathrm{Fin}}^{\mathrm{II}}\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$
3		fin34	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
4	1 2 3	3syl	$$⊢A\in \mathrm{Fin}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
5		isfin4p1	$$⊢A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
6	4 5	sylib	$$⊢A\in \mathrm{Fin}\to A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
7		canthp1	$$⊢1_{𝑜}\prec A\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A$$
8	6 7	anim12i	$$⊢\left(A\in \mathrm{Fin}\wedge 1_{𝑜}\prec A\right)\to \left(A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\wedge \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A\right)$$