Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Eight inequivalent definitions of finite set
cfin7
Next ⟩
df-fin1a
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cfin7
Description:
Extend class notation to include the class of VII-finite sets.
Ref
Expression
Assertion
cfin7
class
Fin
VII