namespace http://mathhub.info/MitM/Foundation/sets ❚

import fnd http://mathhub.info/MitM/Foundation ❚

theory Classes : fnd:?Logic =
    class : type ❙
    cls_element : class ⟶ class ⟶ prop ❘ # 1 ∈ 2 prec -1 ❙

    axiom_extensionality : {s,t} ⊦ (∀[e] e ∈ s ⇔ e ∈ t) ⇒ s ≐ t ❘ # axiom_extensionality 1 2 ❙

    include ☞fnd:?Subtyping ❙
    include ☞fnd:?InformalProofs ❙
    include ☞fnd:?DescriptionOperator ❙

    set = ⟨ s : class | ⊦ ∃ [C : class] s ∈ C ⟩ ❘ # set prec -1 ❙

    emptyclass : set ❘ # ∅ prec -1 ❙
	axiom_emptyClassIsEmpty : {s} ⊦ ¬ s ∈ ∅ ❘ # axiom_emptyClassIsEmpty 1 ❙
❚

// implicit view ZFinNBG : ?ZFBase -> ?Classes =
    include ☞fnd:?InformalProofs ❙
    include ☞fnd:?DescriptionOperator ❙
    set = set ❙
    element = [s,t] cls_element s t ❙
    emptyset = emptyclass ❙
    axiom_emptySetIsEmpty = [s: set] axiom_emptyClassIsEmpty s ❙

    axiom_extensionality = [s,t] sketch "from extensionality" ❙
    axiom_separation = [P,s] sketch "axiomatically" ❙
    axiom_regularity = [s] sketch "axiomatically" ❙
    axiom_pairing = [s,t] sketch "axiomatically" ❙
    axiom_union = [s] sketch "axiomatically" ❙
    axiom_powerset = [s] sketch "axiomatically" ❙
    axiom_replacement = [a,f] sketch "axiomatically" ❙

❚