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

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

theory Sets : fnd:?Logic =
	set : type ❙
	element : set ⟶ set ⟶ prop ❘ # 1 ∈ 2 ❙
	
	emptyset : set ❘ # ∅ ❙

	axiom_emptySetIsEmpty : {s} ⊦ ¬ s ∈ ∅ ❙

	subset : set ⟶ set ⟶ prop ❘ = [s,t] ∀ [z] z ∈ s ⇒ z ∈ t ❘ # 1 ⊑ 2 ❙
	disjoint : set ⟶ set ⟶ prop ❘ = [s,t] ¬∃[e] e ∈ s ∧ e ∈ t ❙
	
	prop_extensionality = [s,t](∀[e] e ∈ s ⇔ e ∈ t) ⇒ s ≐ t ❙
	prop_separation : (set ⟶ prop) ⟶ set ⟶ prop ❘ = [P][s]∃![t]∀[e]e ∈ t ⇔ (e ∈ s ∧ P e) ❙
	prop_regularity = [s]s ≠ ∅ ⇒ ∃ [e] e ∈ s ∧ (disjoint s e) ❙
	prop_pairing = [x,y] ∃[z] x ∈ z ∧ y ∈ z ❙
	prop_pairing_unique = [x,y] ∃![z] x ∈ z ∧ y ∈ z ∧ ∀[w] w ∈ z ⇒ (w ≐ x ∨ w ≐ y) ❙
	prop_union = [x] ∃![y]∀[z] z ∈ y ⇔ ∃[w] z ∈w ∧ w ∈ x ❙
	prop_powerset = [x]∃![y] ∀[z] z ∈ y ⇔ z ⊑ x ❙
	prop_replacement = [A][f : set ⟶ set] ∃![B]∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a) ❙
❚

theory Extensionality : fnd:?Logic =
	include ?Sets ❙
	
	axiom_extensionality : {s,t} ⊦ prop_extensionality s t ❙
❚

theory Separation : fnd:?Logic =
	include ?Sets ❙
	include ☞fnd:?DescriptionOperator ❙
	
	axiom_separation : {P,s} ⊦ prop_separation P s ❘ # axiom_separation 1 2❙
	sep_constructor : {s : set,P : set ⟶ prop}set ❘ = [s,P] that set ([x] ∀[e]e ∈ x ⇔ (e ∈ s ∧ P e)) (axiom_separation P s)❘ # ⟪ 1 | 2 ⟫ prec -1 ❙
❚

theory Intersection : fnd:?Logic =
    include ?Separation ❙

    intersect : set ⟶ set ⟶ set ❘ = [s,t] ⟪ s | ([x] x ∈ t) ⟫ ❘ # 1 ∩ 2 ❙
❚

theory Regularity : fnd:?Logic =
	include ?Sets ❙
	
	axiom_regularity : {s} ⊦ prop_regularity s ❙
❚

theory Pairing : fnd:?Logic =
	include ?Sets ❙
	include ☞fnd:?InformalProofs ❙
	include ☞fnd:?DescriptionOperator ❙

	axiom_pairing : {x,y} ⊦ prop_pairing x y ❙
	lemma_pairing_unique : {x,y : set} ⊦ prop_pairing_unique x y ❘ # axiom_pairing_unique 1 2 ❘ = [x,y] sketch "provable" ❙
	uopair : set ⟶ set ⟶ set ❘ = [x,y] that set ([z] x ∈ z ∧ y ∈ z ∧ ∀[w] w ∈ z ⇒ (w ≐ x ∨ w ≐ y)) (lemma_pairing_unique x y) ❙
	singleton : set ⟶ set ❘ = [s] uopair s s ❙
❚

theory KuratowskiPairs : fnd:?Logic =
	include ?Pairing ❙

	pair : set ⟶ set ⟶ set ❘ = [x,y] uopair (uopair x y) x ❙
❚

theory Union : fnd:?Logic =
	include ?Sets ❙
	include ☞fnd:?DescriptionOperator ❙
	
	axiom_union : {x} ⊦ prop_union x ❘ # axiom_union 1❙
	union : set ⟶ set ❘ = [s] that set ([x] ∀[z] z ∈ x ⇔ ∃[w] z ∈w ∧ w ∈ s) (axiom_union s) ❘ # ⋃ 1 ❙
❚

theory BinaryUnion : fnd:?Logic =
	include ?KuratowskiPairs ❙
	include ?Union ❙
	
	binaryunion : set ⟶ set ⟶ set ❘ = [a,b] ⋃ (uopair a b) ❘ # 1 ∪ 2❙
❚

theory Powerset : fnd:?Logic =
	include ?Sets ❙
	include ☞fnd:?DescriptionOperator ❙
	
	axiom_powerset : {x} ⊦ prop_powerset x ❘ # axiom_powerset 1❙
	powerset : set ⟶ set ❘ = [x] that set ([y] ∀[z] z ∈ y ⇔ z ⊑ x) (axiom_powerset x) ❘ # ℘ 1 ❙
❚

theory CartesianProduct : fnd:?Logic =
	include ?Powerset ❙
	include ?Separation ❙
	include ?BinaryUnion ❙
	
	product : set ⟶ set ⟶ set ❘ = [A,B] sep_constructor (℘ (℘ (A ∪ B))) ([p] ∃[a]∃[b] a ∈ A ∧ b ∈ B ∧ p ≐ pair a b) ❙
❚

theory Relations : fnd:?Logic =
	include ?CartesianProduct ❙
	include ☞fnd:?Subtyping ❙
	
	prop_relation = [s,A,B : set] s ⊑ (product A B) ❘ # prop_relation 1 2 3❙
	relation : set ⟶ set ⟶ type ❘= [A,B] ⟨ s : set | ⊦ prop_relation s A B ⟩ ❙
❚

theory Functions : fnd:?Logic =
	include ?Relations ❙
	include ☞fnd:?InformalProofs ❙
	
	prop_function = [f,A,B] prop_relation f A B ∧ ∀[x] x ∈ A ⇒ ∃[y] y ∈ B ∧ (pair x y) ∈ f ❙ 
	// TODO ❙
	function : set ⟶ set ⟶ type ❘= [A,B] ⟨ s:set | ⊦ prop_function s A B ⟩ ❙
	setfunapply : {A,B} function A B ⟶ {a : set}⊦ a ∈ A ⟶ set ❘ = [A,B,f,a,p] ι ([x] (pair a x) ∈ f) ❘ # 3 @ 4 %I5 ❙
	theorem_setfun : {A,B,f : function A B, a} ⊦ (f @ a) ∈ B ❘ = [A,B,f,a] sketch "by definition" ❙
❚

theory Replacement : fnd:?Logic =
	include ?Sets ❙
	include ☞fnd:?DescriptionOperator ❙
	
	axiom_replacement : {a,f} ⊦ prop_replacement a f ❘ # axiom_replacement 1 2❙
	replacement : set ⟶ (set ⟶ set) ⟶ set ❘ = [A,f] that set ([B] ∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a)) (axiom_replacement A f) ❘ # Img 2 of 1 ❙
❚

theory Infinity : fnd:?Logic =
	include ?BinaryUnion ❙

	set_succ = [n] n ∪ (singleton n) ❙
	prop_infinity = [N] ∅ ∈ N ∧ ∀[n] n ∈ N ⇒ (set_succ n) ∈ N ❙
	omega : set ❘ # ω ❘ = ι [x] prop_infinity x ∧ ∀[z] prop_infinity z ⇒ x ⊑ z❙
❚

theory ZFBase : fnd:?Logic =
    include ?Extensionality ❙
	include ?Separation ❙
	include ?Regularity ❙
	include ?Pairing ❙
	include ?Union ❙
	include ?Powerset ❙
	include ?Replacement ❙
	include ?Infinity ❙
❚

theory FunctionsExtended : fnd:?Logic =
    include ?Functions ❙

    prop_injective : {A,B} function A B ⟶ prop ❘ = [A,B,f] ∀[x] ∀[y] x ∈ A ∧ y ∈ A ⇒ (f@x ≐ f@y ⇒ x ≐ y) ❘ # prop_injective 3 ❙
    prop_surjective : {A,B} function A B ⟶ prop ❘ = [A,B,f] ∀[y] y ∈ B ⇒ ∃[x] x ∈ A ∧ f@x ≐ y ❘ # prop_surjective 3 ❙
    prop_bijective : {A,B} function A B ⟶ prop ❘ = [A,B,f] prop_injective f ∧ prop_surjective f ❘ # prop_bijective 3 ❙
❚

theory Finite : fnd:?Logic =
    include ?FunctionsExtended ❙
    include ?Infinity ❙

    prop_finite : set ⟶ prop ❘ = [s] ∃[n] n ∈ ω ∧ ∃[f : function s n] prop_injective f ❙
    prop_infinite : set ⟶ prop ❘ = [s] ¬ prop_finite s ❙
❚

theory ZF : fnd:?Logic =
    include ?ZFBase ❙
    include ?Finite ❙
    include ?Intersection ❙

	setdiff : set ⟶ set ⟶ set ❘= [A,B] ⟪ A | ([x] ¬ x ∈ B) ⟫ ❘ # 1 \ 2 ❙
	subtract : set ⟶ set ⟶ set ❘= [A,a] A \ (singleton a) ❘ # 2 - 3 ❙
	symdiff : set ⟶ set ⟶ set ❘= [A,B] (A \ B) ∪ (B \ A) ❘ # 2 Δ 3 ❙
❚

theory Choice : fnd:?Logic =
	include ?Functions ❙
	prop_choiceFunction = [A,f : function A (⋃ A)] ∀[a] a ∈ A ⇒ (f @ a) ∈ a ❙
	choice : {A} ⟨ f : function A (⋃A) | ⊦ prop_choiceFunction A f ⟩ ❙
❚

theory ZFCBase : fnd:?Logic =
    include ?ZFBase ❙
    include ?Choice ❙
❚

theory ZFC : fnd:?Logic =
    include ?ZFCBase ❙
    include ?ZF ❙
❚