Description: Obsolete version of 0fi as of 13-Jan-2025. (Contributed by FL, 14-Jul-2008) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0finOLD | |- (/) e. Fin |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano1 | |- (/) e. _om |
|
| 2 | ssid | |- (/) C_ (/) |
|
| 3 | ssnnfi | |- ( ( (/) e. _om /\ (/) C_ (/) ) -> (/) e. Fin ) |
|
| 4 | 1 2 3 | mp2an | |- (/) e. Fin |