namespace latin:/❚

theory SetFOL : ur:?LF =
  include ?FOLEQND❙
  set = term❙
  include ?InternalTypes❙
  include ?Description❙
  include ?RelativizedUniversalQuantificationND❙
  include ?RelativizedExistentialQuantificationND❙
❚

fixmeta ?SetFOL❚

theory Empty =
  isempty : set ⟶ prop❘= [x] ¬ ∃[y] y ∈ x❙
  empty : set❘# ∅❙
  empty_prop : ⊦ isempty ∅❙
  emptyE : {x} ⊦ x∈∅ ⟶ ↯❘= [x,p] empty_prop notE (existsI x p)❙
❚

theory UnorderedPairs =
  uopair : set ⟶ set ⟶ set❙
  uopairIL : {X,Xˈ} ⊦ X ∈ uopair X Xˈ❙
  uopairIR : {X,Xˈ} ⊦ X ∈ uopair X Xˈ❙
  uopairE  : {U,X,Xˈ} ⊦ U ∈ uopair X Xˈ ⟶ ⊦ U≐X ∨ U≐Xˈ❙
❚

theory Singletons =
  singleton : set ⟶ set❙
  singletonI : {x} ⊦ x ∈ singleton x❙
  singletonE : {x,u} ⊦ u ∈ singleton x ⟶ ⊦ u≐x❙
  
  issingleton : set ⟶ prop❘= [x] ∃¹[u]u∈x❙
  singleton_the : {x} ⊦ issingleton x ⟶ set❘= [x,p] the ([u] u ∈ x) p❙
❚

view SelfPair : ?Singletons → ?UnorderedPairs =
  singleton = [x] uopair x x❙
  singletonI = [x] uopairIL❙
  singletonE = [x,u,p] uopairE p orE ([q] q) ([q] q)❙
❚

theory Comprehension =
  comprehend  : set ⟶ (set ⟶ prop) ⟶ set❘# 1 | 2 prec 40❙
  comprehendI : {A,P,X} ⊦ X∈A ⟶ ⊦ P X ⟶ ⊦ X ∈ A|P❙
  comprehend_sub : {A,P,X} ⊦ X ∈ A|P ⟶ ⊦ X∈A❙
  comprehendE : {A,P,X} ⊦ X ∈ A|P ⟶ ⊦ P X❙
❚

theory Replacement =
  replace  : set ⟶ (set ⟶ set) ⟶ set❘# 1 map 2 prec 40❙
  replaceI : {A,F,X} ⊦ X∈A ⟶ ⊦ (F X) ∈ A map F❙
  replaceE : {A,F,X} ⊦ X ∈ A map F ⟶ ⊦ ∃'A [x] (F x) ≐ X❙
❚

theory BigUnion =
  bigunion : set ⟶ set❘# ⋃ 1❙
  bigunionI : {A,X,x} ⊦ x∈X ⟶ ⊦ X∈A ⟶ ⊦ x ∈ ⋃A❙
  bigunionE : {A,X,x,C} ⊦ x ∈ ⋃A ⟶ (⊦ X∈A ⟶ ⊦ x∈X ⟶ ⊦ C) ⟶ ⊦ C❙
❚

theory PowerSets =
  power : set ⟶ set❘# ℘ 1 prec 60❙
  powerI : {X,A} ({u} ⊦u∈X ⟶ ⊦u∈A) ⟶ ⊦X∈℘ A❙
  powerE : {X,A} ⊦X∈℘A ⟶ {u} ⊦u∈X ⟶ ⊦u∈A❙
❚

theory Infinite =
❚