Theorem fingch

Description: A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	fingch	$$⊢\mathrm{Fin}\subseteq \mathrm{GCH}$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢\mathrm{Fin}\subseteq \mathrm{Fin}\cup \left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}$$
2		df-gch	$$⊢\mathrm{GCH}=\mathrm{Fin}\cup \left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}$$
3	1 2	sseqtrri	$$⊢\mathrm{Fin}\subseteq \mathrm{GCH}$$