Description: Once we allow AC, the "strongest" definition of finite set becomes equivalent to the "weakest" and the entire hierarchy collapses. (Contributed by Stefan O'Rear, 29-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | fin71ac | |- Fin7 = Fin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axac3 | |- CHOICE |
|
2 | dfacfin7 | |- ( CHOICE <-> Fin7 = Fin ) |
|
3 | 1 2 | mpbi | |- Fin7 = Fin |