Theorem fingch

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

	Ref	Expression
Assertion	fingch	⊢ Fin ⊆ GCH

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ Fin ⊆ ( Fin ∪ { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥 ) } )
2		df-gch	⊢ GCH = ( Fin ∪ { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥 ) } )
3	1 2	sseqtrri	⊢ Fin ⊆ GCH