namespace http://mathhub.info/Tutorials/Mathematicians ❚

theory ZFC : ?FOLNatDed =
	element : ι ⟶ ι ⟶ prop ❘ # 1 ∈ 2 ❙
	subset : ι ⟶ ι ⟶ prop ❘ = [a,b] ∀[x] x ∈ a ⟹ x ∈ b ❘ # 1 ⊑ 2❙
	
	extensionality : ⊦ ∀[x]∀[y] x ≐ y ⟺ ∀[z] (z ∈ x ⟺ z ∈ y) ❙
	comprehension : ι ⟶ (ι ⟶ prop) ⟶ ι ❘ # ⟨ 1 | 2 ⟩ prec 1 ❙
	separation: {P : ι ⟶ prop} ⊦ ∀[x]∀[z] z ∈ ⟨ x | P ⟩ ⟺ z ∈ x ∧ P z ❙
	
	anyset : ι ❙
	emptyset = ⟨ anyset | ([x] ⊥) ⟩ ❘ # ∅ ❙
	
	pairset : ι ⟶ ι ⟶ ι ❘ # uopair 1 2 prec 1 ❙
	pairing : ⊦ ∀[x]∀[y] ∀[w] w ∈ uopair x y ⟺ w ≐ x ∨ w ≐ y ❙
	pair : ι ⟶ ι ⟶ ι ❘ = [a,b] pairset (pairset a b) (pairset a a) ❙
	
	union : ι ⟶ ι ❘ # ⋃ 1 prec 1 ❙
	axiom_union : ⊦ ∀[x]∀[z](∃[w] z ∈ w ∧ w ∈ x) ⟺ z ∈ ⋃ x ❙
	binary_union : ι ⟶ ι ⟶ ι ❘ # 1 ∪ 2 ❘ = [a,b] ⋃ (pairset a b) ❙
	intersection : ι ⟶ ι ❘ # ⋂ 1 ❘ = [a] ⟨ ⋃ a | ([x] ∀[z] z ∈ a ⟹ x ∈ z) ⟩ ❙
	binary_intersection : ι ⟶ ι ⟶ ι ❘ # 1 ∩ 2 ❘ = [a,b] ⟨ a | ([x] x ∈ b) ⟩ ❙
	
	powerset : ι ⟶ ι ❘ # ℘ 1 prec 1 ❙ // jpow	❙ // \mathcal P ❙
	axiom_powerset : ⊦ ∀[x]∀[z] z ⊑ x ⟺ z ∈ ℘ x ❙
	
	cartesian_product : ι ⟶ ι ⟶ ι ❘ # 1 × 2 prec 1❘
		= [a,b] ⟨ ℘ (℘ (a ∪ b)) | ([z] ∃[v]∃[w] z ≐ pair v w ∧ v ∈ a ∧ w ∈ b) ⟩ ❙
	
	function : ι ⟶ ι ⟶ ι ⟶ prop ❘ # 1 $ 2 -> 3 prec 1❘
		= [f,a,b] f ⊑ (a × b) ∧ ∀[x]x ∈ a ⟹ ∃![y] (pair x y) ∈ f ❙
	
	image : (ι ⟶ ι) ⟶ ι ⟶ ι ❘ # im 1 2 prec 1 ❙
	axiom_replacement : {f : ι ⟶ ι} ⊦ ∀[x]∀[z] (f z) ∈ (im f x) ⟺ z ∈ x ❙
❚