Metamath Proof Explorer

Theorem fingch

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

Ref Expression
Assertion fingch 
|- Fin C_ GCH

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  Fin C_ ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
2 df-gch 
 |-  GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
3 1 2 sseqtrri 
 |-  Fin C_ GCH