Sets, Pairs and Functions

Chad E. Brown, August 2013.

To process this file, Coq must be used with no initial state (i.e., start Coq with the -nois option).

ZF without infinity

Parameter set : Type.

Russell-Prawitz Definitions of Logical Constants.

Definition False : Prop := ∀ P:Prop, P.

Definition not : Prop→Prop := fun A:Prop ⇒ A → False.

Notation "~ x" := (not x) (at level 75, right associativity).

Definition and : Prop→Prop→Prop := fun A B:Prop ⇒ ∀ P:Prop, (A → B → P) → P.

Notation "A /\ B" := (and A B) (at level 80).

Theorem andI : ∀ (A B : Prop), A → B → A ∧ B.

Definition or : Prop→Prop→Prop := fun (A B : Prop) ⇒ ∀ P:Prop, (A → P) → (B → P) → P.

Notation "A \/ B" := (or A B) (at level 85).

Theorem orIL : ∀ (A B : Prop), A → A ∨ B.

Theorem orIR : ∀ (A B : Prop), B → A ∨ B.

Definition iff : Prop→Prop→Prop := fun (A B:Prop) ⇒ (A → B ) ∧ (B → A ).

Notation "A <-> B" := (iff A B) (at level 95).

Theorem iffI : ∀ A B:Prop, (A → B) → (B → A) → (A ↔ B).

Equality can be defined polymorphically as Leibniz equality. As we will only need equality at the type of sets, we only define equality on sets using Leibniz equality.

Definition eq : set→set→Prop := fun (x y : set) ⇒ ∀ Q:set → Prop, Q x → Q y.

Notation "x = y" := (eq x y) (at level 70).
Notation "x <> y" := (¬ x = y) (at level 70).

Theorem eqI : ∀ x:set, x = x.

Theorem eq_sym : ∀ x y:set, x = y → y = x.

Existentials can also be defined polymorphically, but we will only need them for sets and for functions from set to set. To emphasize this, we define existential quantification separately for these two instance types.

Definition ex : (set→Prop)->Prop := fun P:set→Prop ⇒ ∀ Q:Prop, (∀ x, P x → Q) → Q.

Notation "'exists' x , p" := (ex (fun x ⇒ p))
  (at level 200, x ident).

Theorem exI : ∀ P:set→Prop, ∀ x:set, P x → ∃ x, P x.

Definition ex_f : ((set→set)->Prop)->Prop := fun P:(set→set)->Prop ⇒ ∀ Q:Prop, (∀ x, P x → Q) → Q.

Notation "'existsf' x , p" := (ex_f (fun x ⇒ p))
  (at level 200, x ident).

Theorem exI_f : ∀ P:(set→set)->Prop, ∀ F:set→set, P F → existsf F, P F.

Definition exu : (set→Prop)->Prop := fun P:set→Prop ⇒ (∃ x, P x) ∧ (∀ x y:set, P x → P y → x = y ).

Notation "'exists!' x , p" := (exu (fun x ⇒ p))
  (at level 200, x ident).

Theorem exuI : ∀ P:set→Prop, (∃ x, P x) → (∀ x y:set, P x → P y → x = y) → ∃! x, P x.

Description Operator

Parameter Descr : ((set→Prop)->set).

Axiom DescrR : ∀ P:set→Prop, (∃! x, P x) → P (Descr P).

Axioms of Set Theory: ZF without Infinity

In is the membership relation on i. We use x :e y as notation to mean "x is a member of y" and x /:e y as notation for "x is not a member of y."

Parameter In:set→set→Prop.

Notation "x ':e' y" := (In x y) (at level 70).
Notation "x '/:e' y" := (¬ (In x y)) (at level 70).

Subq is the subset relation on set. We use X c= Y as notation to mean "X is a subset of Y" and X /c= Y as notation for "X is not a subset of Y."

Definition Subq : set→set→Prop :=
fun X Y ⇒ ∀ x:set, x :e X → x :e Y.

Notation "X 'c=' Y" := (Subq X Y) (at level 70).
Notation "X '/c=' Y" := (¬ (Subq X Y)) (at level 70).

Lemma Subq_ref : ∀ X:set, X c = X.

Lemma Subq_tra : ∀ X Y Z:set, X c = Y → Y c = Z → X c = Z.

Two sets are equal if they have the same elements. Equivalently, we can always prove two sets are equal by proving they are subsets of each other.

Axiom set_ext : ∀ X Y:set, X c = Y → Y c = X → X = Y.

Sets are formed iteratively, so we can prove Properties about all sets by induction on membership. Suppose P is a Property of sets. If we can prove P holds for X from the inductive hypothesis that P holds for all member of X, then P must hold for all sets.

Axiom In_ind : ∀ P:set→Prop, (∀ X:set, (∀ x, x :e X → P x) → P X) → ∀ X:set, P X.

Empty is the empty set.

Parameter Empty : set.

Axiom EmptyAx : ¬ ∃ x, x :e Empty.

Lemma EmptyE : ∀ x:set, x /:e Empty.

Given a set X, (Union X) is the set {x | there is some Y such that x :e Y and Y :e X}. That is, Union gives the union of a set of sets.

Parameter Union : set→set.

Axiom UnionEq : ∀ X:set, ∀ x:set, x :e Union X ↔ ∃ Y, x :e Y ∧ Y :e X.

Lemma UnionE :
∀ X x:set, x :e (Union X ) → ∃ Y, x :e Y ∧ Y :e X.

Lemma UnionI :
∀ X x Y:set, x :e Y → Y :e X → x :e (Union X ).

(Power X) is the set of all subsets of X.

Parameter Power : set→set.

Axiom PowerEq : ∀ X Y:set, Y :e Power X ↔ Y c = X.

Lemma PowerE : ∀ X Y:set, Y :e Power X → Y c = X.

Lemma PowerI : ∀ X Y:set, Y c = X → Y :e (Power X ).

In classical set theory, Separation follows from Replacement. Separation does not generally follow from Replacement in intuitionistic set theory, although there are alternative formulations of Replacement which are intuitionistically equivalent to the combination of Separation and Replacement as used here.

Parameter Sep : set → (set → Prop) → set.

Notation "{ x :i X | P }" := (Sep X (fun x:set ⇒ P)).

Axiom SepEq : ∀ X:set, ∀ P:set → Prop, ∀ x, x :e {z :i X | P z} ↔ x :e X ∧ P x.

Lemma SepI : ∀ X:set, ∀ P:set → Prop, ∀ x:set,
x :e X → P x → x :e {z :i X |P z}.

Lemma SepE : ∀ X:set, ∀ P:set → Prop, ∀ x:set,
x :e {z :i X |P z} → x :e X ∧ P x.

Lemma SepE1 : ∀ X:set, ∀ P:set → Prop, ∀ x:set,
x :e {z :i X |P z} → x :e X.

Lemma SepE2 : ∀ X:set, ∀ P:set → Prop, ∀ x:set,
x :e {z :i X |P z} → P x.

Given a set X and a function F, (Repl X F) is the set {F x|x :e X}. That is, Repl allows us to form a set by replacing the elements x in a set X with corresponding elements F x. I write (Repl X F) in the eta-expanded form (Repl X (fun z => F z)) just so I can legitimately use the binder notation in the written description.

Parameter Repl : set->(set→set)->set.

Notation "{ F | x :i X }" := (Repl X (fun x:set ⇒ F)).

Axiom ReplEq :
∀ X:set, ∀ F:set→set, ∀ y:set, y :e {F z|z :i X } ↔ ∃ x, x :e X ∧ y = F x.

Lemma ReplE :
∀ X:set, ∀ F:set→set, ∀ y:set, y :e {F z|z :i X } → ∃ x, x :e X ∧ y = F x.

Lemma ReplI :
∀ X:set, ∀ F:set→set, ∀ x:set, x :e X → F x :e {F x |x :i X }.

Lemma Subq_Empty : ∀ X:set, Empty c = X.

Lemma Empty_Power : ∀ X:set, Empty :e Power X.

Lemma In_Power : ∀ X:set, X :e Power X.

Lemma Repl_restr_1 : ∀ X:set, ∀ F G:set → set, (∀ x, x :e X → F x = G x) → {F x|x :i X } c = {G x|x :i X }.

Lemma Repl_restr : ∀ X:set, ∀ F G:set → set, (∀ x, x :e X → F x = G x) → {F x|x :i X } = {G x|x :i X }.

Lemma Repl_Empty : ∀ F:set → set, {F x|x :i Empty } = Empty.

Given two sets y and z, (UPair y z) is {y,z}. Unordered pairs are often taken as primitives in ZF, but they are definable from the primitives above. Zermelo 1930 pointed this out in classical ZF. The argument is given in Suppes 1960;Dover version 1972 and formalized in Isabelle-ZF by Paulson 1993. The argument in the classical case is a little simpler since (Power (Power Empty)) is a two element set. In the intuitionistic case, we use separation to extract a two element subset of (Power (Power Empty)) before using replacement.

Definition TSet : set := {X :i Power (Power Empty) | Empty :e X ∨ Empty /:e X}.
Definition UPair : set→set→set :=
fun y z:set ⇒
{Descr (fun w:set ⇒ ∀ p:set→Prop, (Empty /:e X → p y) → (Empty :e X → p z) → p w)|X :i TSet }.

Notation "{ x , y }" := (UPair x y).

Lemma UPairE :
∀ x y z:set, x :e {y ,z } → x = y ∨ x = z.

Lemma UPairI1 :
∀ y z:set, y :e {y ,z }.

Lemma UPairI2 :
∀ y z:set, z :e {y ,z }.

Lemma UPairEq :
∀ x y z, x :e {y ,z } ↔ x = y ∨ x = z.

Definition Sing : set→set := fun y:set ⇒ {y ,y }.

Notation "{| y |}" := (Sing y).

Lemma SingI : ∀ y, y :e {| y |}.

Lemma SingE : ∀ x y, x :e {| y |} → x = y.

Lemma SingEq : ∀ x y, x :e {| y |} ↔ x = y.

Given sets X and Y, binunion X Y is the binary union of X and Y.

Definition binunion : set → set → set := fun X Y ⇒ Union {X ,Y }.

Notation "X :u: Y" := (binunion X Y) (at level 40).

Lemma binunionI1 : ∀ X Y z, z :e X → z :e X :u : Y.

Lemma binunionI2 : ∀ X Y z, z :e Y → z :e X :u : Y.

Lemma binunionE : ∀ X Y z, z :e X :u : Y → z :e X ∨ z :e Y.

Lemma binunionEq : ∀ X Y z, z :e X :u : Y ↔ z :e X ∨ z :e Y.

Given sets X and Y, setminus X Y is {x :e X | x /:e Y}.

Definition setminus : set → set → set := fun X Y ⇒ {x :i X | x /:e Y }.

Notation "X \ Y" := (setminus X Y) (at level 40).

Lemma setminusI : ∀ X Y z, z :e X → z /:e Y → z :e X \ Y.

Lemma setminusE1 : ∀ X Y z, z :e X \ Y → z :e X.

Lemma setminusE2 : ∀ X Y z, z :e X \ Y → z /:e Y.

Lemma setminusEq : ∀ X Y z, z :e X \ Y ↔ z :e X ∧ z /:e Y.

Given a set X and a function F from sets to sets, famunion X F is the union of all F x where x ranges over X.

Definition famunion : set → (set → set) → set :=
fun X F ⇒ Union {F x|x :i X }.

Notation "'U' x : X , F" := (famunion X (fun x ⇒ F))
(at level 200, x ident).

Lemma famunionI : ∀ X:set, ∀ F:set → set, ∀ x y:set, x :e X → y :e (F x ) → y :e U x:X , F x.

Lemma famunionE : ∀ X:set, ∀ F:set → set, ∀ y:set, y :e (U x:X , F x) → ∃ x, x :e X ∧ y :e (F x).

Lemma famunionEq : ∀ X:set, ∀ F:set → set, ∀ y:set, y :e (U x:X , F x) ↔ ∃ x, x :e X ∧ y :e (F x).

Natural Numbers as Finite Ordinals

Given a set X, ordsucc X is X union {X}.

Definition ordsucc : set→set := fun X ⇒ X :u : {|X |}.

Notation "n +" := (ordsucc n) (at level 20).

Lemma ordsucc_Subq : ∀ X:set, X c = X +.

Lemma ordsucc_in : ∀ X:set, X :e X +.

Lemma ordsuccE : ∀ X z:set, z :e X + → z :e X ∨ z = X.

Opaque ordsucc.

Notation "0" := Empty.
Notation "1" := (0+).
Notation "2" := (1+).

Lemma in_0_1 : 0 :e 1.

Lemma in_0_2 : 0 :e 2.

Lemma in_1_2 : 1 :e 2.

Lemma neq_0_1 : 0 ≠ 1.

Lemma in_1_E : ∀ X:set, X :e 1 → X = 0.

Lemma in_1_Eq : ∀ X:set, X :e 1 ↔ X = 0.

Lemma eq_1_Sing0 : 1 = {|0|}.

Lemma in_2_E : ∀ X:set, X :e 2 → X = 0 ∨ X = 1.

Lemma in_2_Eq : ∀ X:set, X :e 2 ↔ X = 0 ∨ X = 1.

Lemma eq_2_Sing0 : 2 = {0,1}.

nat_p is the least predicate including 0 and closed under ordsucc. nat_p X holds if and only if X is a finite ordinal.

Definition nat_p (n:set) : Prop :=
∀ p:set→Prop, p 0 → (∀ n, p n → p (n +)) → p n.

Lemma nat_0 : nat_p 0.

Lemma nat_ordsucc : ∀ n:set, nat_p n → nat_p (n +).

Lemma nat_1 : nat_p 1.

Lemma nat_2 : nat_p 2.

Lemma nat_ind : ∀ p:set→Prop, p 0 → (∀ n, nat_p n → p n → p (n +)) → ∀ n, nat_p n → p n.

Lemma nat_inv : ∀ n, nat_p n → n = 0 ∨ ∃ m, nat_p m ∧ n = m+.

Lemma nat_complete_ind : ∀ p:set→Prop, (∀ n, nat_p n → (∀ m, m :e n → p m) → p n) → ∀ n, nat_p n → p n.

Lemma nat_0_in_ordsucc : ∀ n, nat_p n → 0 :e n +.

Lemma nat_in_nat : ∀ n, nat_p n → ∀ m, m :e n → nat_p m.

Lemma nat_trans : ∀ n, nat_p n → ∀ m, m :e n → m c = n.

Lemma nat_ordsucc_in_ordsucc : ∀ n, nat_p n → ∀ m, m :e n → m + :e n +.

Membership on natural numbers is decidable.

Lemma nat_in_dec : ∀ n, nat_p n →
∀ m, nat_p m → m :e n ∨ m /:e n.

Epsilon Recursion

Section EpsilonRec.
Variable Phi:set → (set → set) → set.

Definition In_rec_G : set → set → Prop :=
fun X Y ⇒
∀ R:set→set→Prop,
(∀ X F, (∀ x, x :e X → R x (F x)) → R X (Phi X F)) →
R X Y.

Definition In_rec : set → set := fun X ⇒ Descr (In_rec_G X).

Lemma In_rec_G_c : ∀ X:set, ∀ F:set→set, (∀ x, x :e X → In_rec_G x (F x)) → In_rec_G X (Phi X F).

Lemma In_rec_G_ind :
∀ R:set → set → Prop,
(∀ X F, (∀ x, x :e X → In_rec_G x (F x) ∧ R x (F x)) → R X (Phi X F)) →
(∀ X Y, In_rec_G X Y → R X Y).

Lemma In_rec_G_inv : ∀ X Y:set, In_rec_G X Y → existsf F, (∀ x, x :e X → In_rec_G x (F x)) ∧ Y = Phi X F.

Definition Cond_Phi : Prop := ∀ X:set, ∀ F G:set → set, (∀ x, x :e X → F x = G x) → Phi X F = Phi X G.

Hypothesis Phir:Cond_Phi.

Lemma In_rec_G_f : ∀ X Y Z:set, In_rec_G X Y → In_rec_G X Z → Y = Z.

Lemma In_rec_G_In_rec : ∀ X:set, In_rec_G X (In_rec X).

Lemma In_rec_G_In_rec_d : ∀ X:set, In_rec_G X (Phi X In_rec).

Lemma In_rec_eq : ∀ X:set, In_rec X = Phi X In_rec.

End EpsilonRec.

Specification for Pairs and Functions

Module Type PairFun.

Parameter pair : set → set → set.

Local Notation "( x , y )" := (pair x y).

Axiom pair_spec : ∀ x y w z:set, (x ,y ) = (w ,z ) ↔ x = w ∧ y = z.

Parameter lam : set → (set → set) → set.

Notation "'lambda' x : X , F" := (lam X (fun x:set ⇒ F))
  (at level 200, x ident).

Axiom lam_spec : ∀ X, ∀ F G:set → set, (∀ x, x :e X → F x = G x ) ↔ (lambda x:X , F x) = (lambda x:X , G x).

Parameter SIGMA : set → (set → set) → set.

Local Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set ⇒ Y))
  (at level 200, x ident).

Axiom pair_SigmaEq : ∀ X:set, ∀ Y:set→set, ∀ z:set, z :e (Sigma x : X , Y x) ↔ ∃ x, x :e X ∧ ∃ y, y :e Y x ∧ z = (x,y).

Parameter PI : set → (set → set) → set.

Notation "'Pi' x : X , Y" := (PI X (fun x:set ⇒ Y))
  (at level 200, x ident).

Axiom lam_PiEq : ∀ X:set, ∀ Y:set → set, ∀ f:set, f :e (Pi x : X , Y x) ↔ existsf F, (∀ x, x :e X → F x :e Y x ) ∧ f = lambda x:X , F x.

Parameter ap : set → set → set.
Axiom beta : ∀ X:set, ∀ F:set → set, ∀ x:set, x :e X → ap (lambda x:X , F x) x = F x.
Axiom ap_Pi : ∀ X:set, ∀ Y:set → set, ∀ f:set, ∀ x:set, f :e (Pi x:X , Y x ) → x :e X → (ap f x ) :e (Y x ).

Axiom lam2_pair : ∀ F, (lambda z:2, F z) = (F 0,F 1).

Axiom beta0 : ∀ X:set, ∀ F:set → set, ∀ x:set, x /:e X → ap (lambda x : X , F x) x = 0.

Axiom Sigma_Power_1 : ∀ X:set, X :e Power 1 → ∀ Y:set→set, (∀ x, x :e X → Y x :e Power 1) → (Sigma x:X , Y x) :e Power 1.

Axiom Pi_Power_1 : ∀ X:set, ∀ Y:set→set, (∀ x, x :e X → Y x :e Power 1) → (Pi x:X , Y x) :e Power 1.

End PairFun.

Consequences of the Specification

These are proven here to make clear that they follow from the specification. The ones I really need are reproven in the implementation because the proofs are sometimes clearer there.

Module PairFunConseq (P:PairFun).
  Import P.

Local Notation "( x , y )" := (pair x y).

Notation "'lambda' x : X , F" := (lam X (fun x:set ⇒ F))
  (at level 200, x ident).

Local Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set ⇒ Y))
  (at level 200, x ident).

Notation "'Pi' x : X , Y" := (PI X (fun x:set ⇒ Y))
  (at level 200, x ident).

Lemma pair_lam2_ex : ∀ x y, existsf F, F 0 = x ∧ F 1 = y ∧ (x ,y ) = lambda z:2, F z.

Local Notation "X * Y" := (Sigma _:X, Y) (at level 40).

Local Notation "X ^ Y" := (Pi _:Y, X) (at level 30).

Lemma setexp_2_eq : ∀ X:set, X × X = X ^ 2.

Lemma pair_ap_0 : ∀ x y:set, ap (x ,y ) 0 = x.

Lemma pair_ap_1 : ∀ x y:set, ap (x ,y ) 1 = y.

Lemma pair_ap_n2 : ∀ x y i:set, i /:e 2 → ap (x ,y ) i = 0.

Lemma ap0_Sigma : ∀ X:set, ∀ Y:set → set, ∀ z:set, z :e (Sigma x:X , Y x) → (ap z 0) :e X.

Lemma ap1_Sigma : ∀ X:set, ∀ Y:set → set, ∀ z:set, z :e (Sigma x:X , Y x) → (ap z 1) :e (Y (ap z 0)).

End PairFunConseq.

Implementation of Pairs and Functions

Module PairFunImpl : PairFun.

Inj1 is an injection of set into itself that will correspond to x |-> (1,x) after pairing is defined.

Definition Inj1 : set → set := In_rec (fun X F ⇒ {| 0 |} :u : {F x|x :i X }).

Lemma Inj1_eq : ∀ X:set, Inj1 X = {| 0 |} :u : {Inj1 x|x :i X }.

Lemma Inj1I1 : ∀ X:set, Empty :e Inj1 X.

Lemma Inj1I2 : ∀ X x:set, x :e X → Inj1 x :e Inj1 X.

Lemma Inj1E : ∀ X y:set, y :e Inj1 X → y = Empty ∨ ∃ x, x :e X ∧ y = Inj1 x.

Inj0 is an injection of set into itself that will correspond to x |-> (0,x) after pairing is defined.

Definition Inj0 : set → set := fun X ⇒ {Inj1 x|x :i X }.

Lemma Inj0I : ∀ X x:set, x :e X → Inj1 x :e (Inj0 X ).

Lemma Inj0E : ∀ X y:set, y :e Inj0 X → ∃ x, x :e X ∧ y = Inj1 x.

Unj is a left inverse of both Inj1 and Inj0.

Definition Unj : set → set := In_rec (fun X F ⇒ {F x|x :i X \ {|0|} }).

Lemma Unj_eq : ∀ X:set, Unj X = {Unj x|x :i X \ {|0|} }.

Lemma Unj_Inj1_eq : ∀ X:set, Unj (Inj1 X) = X.

Lemma Inj1_inj : ∀ X Y:set, Inj1 X = Inj1 Y → X = Y.

Lemma Unj_Inj0_eq : ∀ X:set, Unj (Inj0 X) = X.

Lemma Inj0_inj : ∀ X Y:set, Inj0 X = Inj0 Y → X = Y.

Lemma Inj0_Inj1_neq : ∀ X Y:set, Inj0 X ≠ Inj1 Y.

Lemma Inj0_0 : Inj0 0 = 0.

Pairing as Disjoint Union

Definition pair : set → set → set := fun X Y ⇒ {Inj0 x|x :i X } :u : {Inj1 y|y :i Y }.

Notation "( x , y )" := (pair x y).

Lemma pair_0_0 : (0,0) = 0.

Lemma pair_0_x : ∀ x, Inj0 x = (0,x ).

Lemma pair_1_x : ∀ x, Inj1 x = (1,x ).

Now that we know pair_0_x and pair_1_x and consequences, we need never use Inj0 or Inj1 again.

Opaque Inj0 Inj1.

Lemma pairI0 : ∀ X Y x, x :e X → (0,x ) :e (X ,Y ).

Lemma pairI1 : ∀ X Y y, y :e Y → (1,y ) :e (X ,Y ).

Lemma pairE : ∀ X Y z, z :e (X ,Y ) → (∃ x, x :e X ∧ z = (0,x)) ∨ (∃ y, y :e Y ∧ z = (1,y)).

Lemma pairEq : ∀ X Y z, z :e (X ,Y ) ↔ (∃ x, x :e X ∧ z = (0,x)) ∨ (∃ y, y :e Y ∧ z = (1,y)).

Lemma pair_0_inj : ∀ x y, (0,x ) = (0,y ) → x = y.

Lemma pair_1_inj : ∀ x y, (1,x ) = (1,y ) → x = y.

Lemma pair_0_1_neq : ∀ x y, (0,x ) ≠ (1,y ).

Lemma pairE0 : ∀ X Y x, (0,x ) :e (X ,Y ) → x :e X.

Lemma pairE1 : ∀ X Y y, (1,y ) :e (X ,Y ) → y :e Y.

Lemma pair_inj_Subq_0 : ∀ x y w z:set, (x ,y ) c = (w ,z ) → x c = w.

Lemma pair_inj_Subq_1 : ∀ x y w z:set, (x ,y ) c = (w ,z ) → y c = z.

Theorem pair_inj : ∀ x y w z:set, (x ,y ) = (w ,z ) → x = w ∧ y = z.

Theorem pair_spec : ∀ x y w z:set, (x ,y ) = (w ,z ) ↔ x = w ∧ y = z.

Functions

Functions are represented following Aczel's trace representation. The exact sets one obtains depends on the representation of pairs.

lam X F is {(x,y) | x :e X, y :e F x}.

Definition lam : set → (set → set) → set :=
fun X F ⇒ U x:X , {(x,y)|y :i F x}.

Notation "'lambda' x : X , F" := (lam X (fun x:set ⇒ F))
(at level 200, x ident).

Lemma lamI : ∀ X:set, ∀ F:set→set, ∀ x y:set, x :e X → y :e F x → (x ,y ) :e lambda x:X , F x.

Lemma lamE : ∀ X:set, ∀ F:set→set, ∀ z:set, z :e (lambda x:X , F x) → ∃ x, x :e X ∧ ∃ y, y :e F x ∧ z = (x,y).

Lemma lamEq : ∀ X:set, ∀ F:set→set, ∀ z:set, z :e (lambda x:X , F x) ↔ ∃ x, x :e X ∧ ∃ y, y :e F x ∧ z = (x,y).

Lemma lamPE : ∀ X:set, ∀ F:set → set, ∀ x y:set, (x ,y ) :e (lambda x:X , F x ) → x :e X ∧ y :e F x.

Lemma lamPEq : ∀ X:set, ∀ F:set → set, ∀ x y:set, (x ,y ) :e (lambda x:X , F x ) ↔ x :e X ∧ y :e F x.

ap f x is {y | (x,y) is in f}, i.e., {the y such that z = (x,y) | z :e f; exists y, z = (x,y)}

Definition ap : set → set → set :=
fun f x ⇒ {Descr (fun y ⇒ z = (x ,y ))|z :i {z :i f |∃ y, z = (x ,y)} }.

Theorem apEq : ∀ f x y, y :e ap f x ↔ (x ,y ) :e f.

Lemma apI : ∀ f x y, (x ,y ) :e f → y :e ap f x.

Lemma apE : ∀ f x y, y :e ap f x → (x ,y ) :e f.

Theorem beta : ∀ X:set, ∀ F:set → set, ∀ x:set, x :e X → ap (lambda x:X , F x) x = F x.

Theorem beta0 : ∀ X:set, ∀ F:set → set, ∀ x:set, x /:e X → ap (lambda x:X , F x) x = 0.

Lemma lam_inj_lem : ∀ X, ∀ F G:set → set, (∀ x, x :e X → F x = G x) → (lambda x:X , F x) c = (lambda x:X , G x).

Lemma lam_inj : ∀ X, ∀ F G:set → set, (∀ x, x :e X → F x = G x) → (lambda x:X , F x) = (lambda x:X , G x).

Theorem lam_spec : ∀ X, ∀ F G:set → set, (∀ x, x :e X → F x = G x ) ↔ (lambda x:X , F x) = (lambda x:X , G x).

Opaque ap lam.

Lemma lam2_pair : ∀ F, (lambda z:2, F z) = (F 0,F 1).

Theorem pair_ap_0 : ∀ x y:set, ap (x ,y ) 0 = x.

Theorem pair_ap_1 : ∀ x y, ap (x ,y ) 1 = y.

Theorem pair_ap_n2 : ∀ x y i:set, i /:e 2 → ap (x ,y ) i = 0.

Sets of Pairs: Sigma as Lambda

Definition SIGMA : set → (set → set) → set := lam.

Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set ⇒ Y))
(at level 200, x ident).

pair_SigmaI is the same as lamI and pair_SigmaE is the same as lamE.

Theorem pair_SigmaI : ∀ X:set, ∀ Y:set → set, ∀ x y:set, x :e X → y :e (Y x ) → (x ,y ) :e (Sigma x:X , Y x ).

Theorem pair_SigmaE : ∀ X:set, ∀ Y:set → set, ∀ u:set, u :e (Sigma x:X , Y x) → ∃ x, x :e X ∧ ∃ y, y :e Y x ∧ u = (x,y).

Theorem pair_SigmaEq : ∀ X:set, ∀ Y:set→set, ∀ z:set, z :e (Sigma x:X , Y x) ↔ ∃ x, x :e X ∧ ∃ y, y :e Y x ∧ z = (x,y).

Lemma ap0_Sigma : ∀ X:set, ∀ Y:set → set, ∀ z:set,
z :e (Sigma x:X , Y x) → (ap z 0) :e X.

Lemma ap1_Sigma : ∀ X:set, ∀ Y:set → set, ∀ z:set,
z :e (Sigma x:X , Y x) → (ap z 1) :e (Y (ap z 0)).

Lemma Sigma_eta : ∀ X:set, ∀ Y:set → set, ∀ z:set,
z :e (Sigma x:X , Y x) → (ap z 0,ap z 1) = z.

Sets of Functions: Pi

PI X Y = {f in (Power (Sigma X (fun x => (Union (Y x))))) | forall x:X, ap f x : Y x}

Definition PI : set → (set → set) → set :=
fun X Y ⇒ {f :i (Power (Sigma x:X , (Union (Y x)))) | ∀ x, x :e X → (ap f x ) :e (Y x )}.

Notation "'Pi' x : X , Y" := (PI X (fun x:set ⇒ Y))
(at level 200, x ident).

Lemma lam_PiI : ∀ X:set, ∀ Y:set → set, ∀ F:set → set,
(∀ x:set, x :e X → (F x ) :e (Y x )) → (lambda x:X , F x) :e (Pi x:X , Y x).

Lemma ap_Pi : ∀ X:set, ∀ Y:set → set, ∀ f:set, ∀ x:set,
f :e (Pi x:X , Y x ) → x :e X → (ap f x ) :e (Y x ).

Lemma Pi_eta : ∀ X:set, ∀ Y:set → set, ∀ f:set,
f :e (Pi x:X , Y x) → (lambda x:X , ap f x) = f.

Lemma lam_PiE : ∀ X:set, ∀ Y:set → set, ∀ f:set, f :e (Pi x:X , Y x) → existsf F, (∀ x, x :e X → F x :e Y x ) ∧ f = lambda x:X , F x.

Lemma lam_PiEq : ∀ X:set, ∀ Y:set → set, ∀ f:set, f :e (Pi x:X , Y x) ↔ existsf F, (∀ x, x :e X → F x :e Y x ) ∧ f = lambda x:X , F x.

Notation "X * Y" := (Sigma _:X, Y) (at level 40).

Notation "X ^ Y" := (Pi _:Y, X) (at level 30).

Lemma setexp_2_eq : ∀ X:set, X × X = X ^ 2.

Closure of Power 1 under Sigma and Pi (with Pi impredicative)

Lemma Sigma_Power_1 : ∀ X:set, X :e Power 1 → ∀ Y:set→set, (∀ x, x :e X → Y x :e Power 1) → (Sigma x:X , Y x) :e Power 1.

Lemma Pi_Power_1 : ∀ X:set, ∀ Y:set→set, (∀ x, x :e X → Y x :e Power 1) → (Pi x:X , Y x) :e Power 1.

Monotonicity Results

Lemma pairSubq : ∀ X Y W Z, X c = W → Y c = Z → (X ,Y ) c = (W ,Z ).

Covariance of subsets of Sigmas

Lemma Sigma_mon : ∀ X Y:set, X c = Y → ∀ Z W:set→set, (∀ x, x :e X → Z x c = W x) → (Sigma x:X , Z x) c = (Sigma y:Y , W y).

Lemma Sigma_mon0 : ∀ X Y:set, X c = Y → ∀ Z:set→set, (Sigma x:X , Z x) c = (Sigma y:Y , Z y).

Lemma Sigma_mon1 : ∀ X:set, ∀ Z W:set→set, (∀ x, x :e X → Z x c = W x) → (Sigma x:X , Z x) c = (Sigma x:X , W x).

Covariance of subsets of function spaces when codomain has 0 as a member. This depends on an assumption about decidability of X relative to Y.

Lemma Pi_0_dom_mon : ∀ X Y:set, ∀ A:set→set,
X c = Y →
(∀ y, y :e Y → y :e X ∨ y /:e X) →
(∀ y, y :e Y → y /:e X → 0 :e A y) →
(Pi x:X , A x) c = (Pi x:Y , A x).

Lemma setexp_0_dom_mon : ∀ A:set, 0 :e A → ∀ X Y:set,
X c = Y →
(∀ y, y :e Y → y :e X ∨ y /:e X) →
A ^ X c = A ^ Y.

Lemma Pi_cod_mon : ∀ X:set, ∀ A B:set→set, (∀ x, x :e X → A x c = B x) → (Pi x:X , A x) c = (Pi x:X , B x).

Lemma Pi_0_mon : ∀ X Y:set, ∀ A B:set→set,
(∀ x, x :e X → A x c = B x) →
X c = Y →
(∀ y, y :e Y → y :e X ∨ y /:e X) →
(∀ y, y :e Y → y /:e X → 0 :e B y) →
(Pi x:X , A x) c = (Pi y:Y , B y).

Lemma setexp_0_mon : ∀ X Y A B:set,
0 :e B → A c = B →
X c = Y →
(∀ y, y :e Y → y :e X ∨ y /:e X) →
A ^ X c = B ^ Y.

Combining transitivity of natural numbers (finite ordinals) with decidability of membership on natural numbers, we know that if 0 is in A, n is a natural number and m is in n (i.e., m < n), then the set of m-tuples from A is a subset of the set of n-tuples from A.

Lemma nat_in_setexp_mon : ∀ A:set, 0 :e A → ∀ n, nat_p n →
∀ m, m :e n → A ^ m c = A ^ n.

Sums are Pairs

Definition sum : set → set → set := pair.

Notation "X :+: Y" := (sum X Y) (at level 50).

These next three are duplicates of pairI0, pairI1 and pairE.

Lemma pair0_sum : ∀ X Y x:set, x :e X → (0,x ) :e X :+: Y.

Lemma pair1_sum : ∀ X Y y:set, y :e Y → (1,y ) :e X :+: Y.

Lemma sum_inv : ∀ X Y z:set, z :e X :+: Y → (∃ x, x :e X ∧ z = (0,x)) ∨ (∃ y, y :e Y ∧ z = (1,y)).

Lemma sumEq : ∀ X Y z, z :e X :+: Y ↔ (∃ x, x :e X ∧ z = (0,x)) ∨ (∃ y, y :e Y ∧ z = (1,y)).

Lemma pair_1_0_1 : (1,0) = 1.

Lemma nat_pair1_ordsucc : ∀ n:set, nat_p n → (1,n ) = ordsucc n.

Lemma nat_sum1_ordsucc : ∀ n:set, nat_p n → 1 :+: n = ordsucc n.

Lemma sum_1_0_1 : 1 :+: 0 = 1.

Lemma pair_1_1_2 : (1,1) = 2.

Lemma sum_1_1_2 : 1 :+: 1 = 2.

Covariance of subsets of sums (same as pairSubq)

Lemma sum_mon : ∀ X Y W Z, X c = W → Y c = Z → X :+: Y c = W :+: Z.

End PairFunImpl.