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 | |- ( ( A e. Fin /\ 1o ~< A ) -> ( A ~< ( A |_| 1o ) /\ ( A |_| 1o ) ~< ~P A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fin12 | |- ( A e. Fin -> A e. Fin2 ) |
|
| 2 | fin23 | |- ( A e. Fin2 -> A e. Fin3 ) |
|
| 3 | fin34 | |- ( A e. Fin3 -> A e. Fin4 ) |
|
| 4 | 1 2 3 | 3syl | |- ( A e. Fin -> A e. Fin4 ) |
| 5 | isfin4p1 | |- ( A e. Fin4 <-> A ~< ( A |_| 1o ) ) |
|
| 6 | 4 5 | sylib | |- ( A e. Fin -> A ~< ( A |_| 1o ) ) |
| 7 | canthp1 | |- ( 1o ~< A -> ( A |_| 1o ) ~< ~P A ) |
|
| 8 | 6 7 | anim12i | |- ( ( A e. Fin /\ 1o ~< A ) -> ( A ~< ( A |_| 1o ) /\ ( A |_| 1o ) ~< ~P A ) ) |