Formal theorems and proofs

Table of contents

  1. Morse-Kelley set theory
    1. Definitions
    2. Axioms
  2. Classical logic
    1. Inference rules
    2. Propositional logic
      1. The relationship of EFQ, LEM, DNE
      2. Useful theorems
      3. De Morgan's laws
      4. Projections
    3. First order logic
      1. Bounded quantification
      2. De Morgan's laws
    4. First order logic with equality
      1. Useful theorems
      2. Unique existence
  3. Basic results
    1. Inclusion
    2. Class comprehension
    3. Binary operations on sets
    4. The empty set
    5. Operations on systems of sets
    6. The universal class and Russell's paradox
    7. Singletons, pair sets and pairs
    8. Operations on families of sets
  4. Relations
    1. Relationhood
    2. Domains and ranges
    3. Images and inverse images
    4. Composition of relations
    5. Special relations
  5. Functions
    1. Functionhood
    2. Function application
    3. Function composition
    4. Restricted functions
    5. Special functions
    6. Partly functional relations
    7. Injections, surjections, bijections
    8. Choice functions
  6. Power sets
  7. Well-founded relations
  8. The natural numbers as ordinals
  9. Closure operators
  10. Grothendieck universes
  11. Cardinal numbers
    1. Numerousities
  12. Ordinal numbers
    1. Transitive sets
    2. Ordinal numbers

Morse-Kelley set theory

Definitions

Definition. incl_equi
A ⊆ B ↔ ∀x. x ∈ A → x ∈ B
Definition. set_equi
set x ↔ ∃C. x ∈ C
Definition. empty_set_eq
∅ = {x | ⊥}
Definition. union_eq
A ∪ B = {x | x ∈ A ∨ x ∈ B}
Definition. sg_eq
{a} = {x | set a → x = a}
Definition. pair_eq
(x, y) = {{x}, {x, y}}
Definition. power_eq
power M = {A | A ⊆ M}
Definition. intersection_eq
A ∩ B = {x | x ∈ A ∧ x ∈ B}
Definition. diff_eq
A \ B = {x | x ∈ A ∧ ¬x ∈ B}
Definition. compl_eq
compl A = {x | ¬x ∈ A}
Definition. Union_eq
⋃M = {x | ∃A. A ∈ M ∧ x ∈ A}
Definition. Intersection_eq
⋂M = {x | ∀A. A ∈ M → x ∈ A}
Definition. prod_eq
A × B = {t | ∃x. ∃y. x ∈ A ∧ y ∈ B ∧ t = (x, y)}
Definition. fst_eq
fst t = ⋂⋂t
Definition. scd_eq
scd t = ⋂⋃t ∪ (⋃⋃t \ ⋂⋂t)
Definition. UnivCl_eq
UnivCl = {x | x = x}
Definition. DiagCl_eq
DiagCl = {x | ¬x ∈ x}
Definition. dom_eq
dom R = {x | ∃y. (x, y) ∈ R}
Definition. rng_eq
rng R = {y | ∃x. (x, y) ∈ R}
Definition. img_eq
img R A = {y | ∃x. x ∈ A ∧ (x, y) ∈ R}
Definition. inv_img_eq
inv_img R B = {x | ∃y. y ∈ B ∧ (x, y) ∈ R}
Definition. app_eq
app f x = ⋂{y | (x, y) ∈ f}
Definition. relation_equi
relation R ↔ ∀t. t ∈ R → ∃x. ∃y. t = (x, y)
Definition. function_equi
function f ↔ relation f ∧ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2
Definition. map_equi
map f X Y ↔ function f ∧ dom f = X ∧ rng f ⊆ Y
Definition. inj_equi
inj f X Y ↔ map f X Y ∧ ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b
Definition. sur_equi
sur f X Y ↔ map f X Y ∧ rng f = Y
Definition. bij_equi
bij f X Y ↔ inj f X Y ∧ sur f X Y
Definition. inv_eq
inv f = {t | ∃x. ∃y. t = (y, x) ∧ (x, y) ∈ f}
Definition. restr_eq
restr f A = f ∩ (A × UnivCl)
Definition. choice_function_equi
choice_function f ↔ function f ∧ ∀x. x ∈ dom f → app f x ∈ x
Definition. composition_eq
g ∘ f = {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ f ∧ (y, z) ∈ g}

Axioms

Axiom. efq
⊥ → A
Axiom. lem
A ∨ ¬A
Axiom. equi_subst
(A ↔ B) → P A → P B
Axiom. eq_refl
x = x
Axiom. eq_subst
x = y → P x → P y
Axiom. ext
(∀x. x ∈ A ↔ x ∈ B) → A = B
Axiom. comp
u ∈ {x | P x} ↔ set u ∧ P u
Axiom. pairing
set x → set y → set {x, y}
Axiom. subset
A ⊆ B → set B → set A
Axiom. power
set M → set (power M)
Axiom. union
set M → set (⋃M)
Axiom. regularity
¬A = ∅ → ∃x. x ∈ A ∧ x ∩ A = ∅
Axiom. infinity
∃A. set A ∧ (∅ ∈ A ∧ ∀x. x ∈ A → x ∪ {x} ∈ A)
Axiom. substitution
function f → set (dom f) → set (rng f)
Axiom. choice
∃f. choice_function f ∧ dom f = UnivCl \ {∅}

Classical logic

Inference rules

Rule. hypo
(⊤ ∧ A ⊢ A)
Rule. conj_intro
(H1 ⊢ A) → (H2 ⊢ B) → (H1 ∧ H2 ⊢ A ∧ B)
Rule. conj_eliml
(H ⊢ A ∧ B) → (H ⊢ A)
Rule. conj_elimr
(H ⊢ A ∧ B) → (H ⊢ B)
Rule. disj_introl
(H ⊢ A) → (H ⊢ A ∨ B)
Rule. disj_intror
(H ⊢ B) → (H ⊢ A ∨ B)
Rule. disj_elim
(H1 ⊢ A ∨ B) → (H2 ∧ A ⊢ C) → (H3 ∧ B ⊢ C) → (H1 ∧ H2 ∧ H3 ⊢ C)
Rule. subj_intro
(H ∧ A ⊢ B) → (H ⊢ A → B)
Rule. subj_elim
(H1 ⊢ A → B) → (H2 ⊢ A) → (H1 ∧ H2 ⊢ B)
Rule. neg_intro
(H ∧ A ⊢ ⊥) → (H ⊢ ¬A)
Rule. neg_elim
(H1 ⊢ ¬A) → (H2 ⊢ A) → (H1 ∧ H2 ⊢ ⊥)
Rule. bij_intro
(H1 ⊢ A → B) → (H2 ⊢ B → A) → (H1 ∧ H2 ⊢ A ↔ B)
Rule. bij_eliml
(H ⊢ A ↔ B) → (H ⊢ A → B)
Rule. bij_elimr
(H ⊢ A ↔ B) → (H ⊢ B → A)
Rule. wk
(H ⊢ B) → (H ∧ A ⊢ B)
Rule. exch
(H ⊢ A) → (H ⊢ A)
Rule. uq_intro
(nf u (H ∧ ∀x. P x)) → (H ⊢ P u) → (H ⊢ ∀x. P x)
Rule. uq_elim
(H ⊢ ∀x. P x) → (H ⊢ P t)
Rule. ex_intro
(H ⊢ P t) → (H ⊢ ∃x. P x)
Rule. ex_elim
(nf u (H1 ∧ H2 ∧ B ∧ ∃x. P x)) → (H1 ⊢ ∃x. P x) → (H2 ∧ P u ⊢ B) → (H1 ∧ H2 ⊢ B)
Rule. subj_intro_ii
(H ∧ A ∧ B ⊢ C) → (H ⊢ A → B → C)
Rule. subj_intro_iii
(H ∧ A ∧ B ∧ C ⊢ D) → (H ⊢ A → B → C → D)
Rule. subj_intro_iv
(H ∧ A ∧ B ∧ C ∧ D ⊢ E) → (H ⊢ A → B → C → D → E)

Propositional logic

The relationship of EFQ, LEM, DNE

Theorem. dne
¬¬A → A
Theorem. efq_from_dne
(¬¬A → A) → (⊥ → A)
Theorem. lem_from_dne
A ∨ ¬A

Useful theorems

Theorem. diag_contra
(A ↔ ¬A) → ⊥
Theorem. dn_intro
A → ¬¬A
Theorem. contraposition
(A → B) → ¬B → ¬A
Theorem. contraposition_rev
(¬A → ¬B) → (B → A)
Theorem. subj_from_disj
(¬A ∨ B) → (A → B)
Theorem. tollendo_ponens_left
A ∨ B → ¬B → A
Theorem. tollendo_ponens_right
A ∨ B → ¬A → B
Theorem. hypothetical_syllogism
(A → B) → (B → C) → (A → C)
Theorem. equi_refl
A ↔ A
Theorem. equi_symm
(A ↔ B) → (B ↔ A)
Theorem. equi_trans
(A ↔ B) → (B ↔ C) → (A ↔ C)

De Morgan's laws

Theorem. neg_conj
¬(A ∧ B) → ¬A ∨ ¬B
Theorem. neg_subj
¬(A → B) → A ∧ ¬B

Projections

Theorem. conj_elimll
A ∧ B ∧ C → A
Theorem. conj_elimlr
A ∧ B ∧ C → B
Theorem. conj_elimrl
A ∧ (B ∧ C) → B
Theorem. conj_elimrr
A ∧ (B ∧ C) → C
Theorem. conj_elimlll
A ∧ B ∧ C ∧ D → A
Theorem. conj_elimllr
A ∧ B ∧ C ∧ D → B
Theorem. lsubj_elim
(A ↔ B) → A → B
Theorem. rsubj_elim
(A ↔ B) → B → A
Theorem. lsubj_conj_eliml
(E ↔ A ∧ B) → E → A
Theorem. lsubj_conj_elimr
(E ↔ A ∧ B) → E → B
Theorem. lsubj_conj_elimll
(E ↔ A ∧ B ∧ C) → E → A
Theorem. lsubj_conj_elimlr
(E ↔ A ∧ B ∧ C) → E → B
Theorem. lsubj_conj_elimlll
(E ↔ A ∧ B ∧ C ∧ D) → E → A
Theorem. lsubj_conj_elimllr
(E ↔ A ∧ B ∧ C ∧ D) → E → B

First order logic

Bounded quantification

Theorem. uq_bounded_elim
(∀x. E x → P x) → E u → P u

De Morgan's laws

Theorem. neg_ex
(¬∃x. P x) → (∀x. ¬P x)
Theorem. neg_uq
(¬∀x. P x) → (∃x. ¬P x)
Theorem. uq_neg
(∀x. ¬P x) → (¬∃x. P x)
Theorem. ex_neg
(∃x. ¬P x) → (¬∀x. P x)
Theorem. neg_uq_bounded
(¬∀x. P x → Q x) → (∃x. P x ∧ ¬Q x)
Theorem. neg_ex_bounded
(¬∃x. P x ∧ Q x) → (∀x. P x → ¬Q x)

First order logic with equality

Useful theorems

Theorem. eq_symm
x = y → y = x
Theorem. eq_subst_rev
y = x → P x → P y
Theorem. f_equal
x = y → f x = f y
Theorem. eq_trans
x = y → y = z → x = z
Theorem. eq_symm_trans
y = x → y = z → x = z
Theorem. neq_symm
¬x = y → ¬y = x
Theorem. disused_eq
(∀x. x = y → A) → A

Unique existence

Theorem. ex_uniq_intro
(∃x. P x) → (∀x. ∀y. P x → P y → x = y) → (∃x. ∀y. x = y ↔ P y)
Theorem. ex_uniq_eliml
(∃x. ∀y. x = y ↔ P y) → (∃x. P x)
Theorem. ex_uniq_elimr
(∃x. ∀y. x = y ↔ P y) → P x → P y → x = y
Theorem. ex_uniq_set_intro
(∃x. S x ∧ P x) → (∀x. ∀y. P x → P y → x = y) → (∃x. S x ∧ ∀y. x = y ↔ P y)
Theorem. ex_uniq_set_elimr
(∃x. S x ∧ ∀y. x = y ↔ P y) → P x → P y → x = y
Theorem. ex_uniq_from_mixed_form
(∃x. S x ∧ P x ∧ ∀y. P y → x = y) → (∃x. S x ∧ ∀y. x = y ↔ P y)
Theorem. ex_weaken_conj
(∀x. P x → Q x) → (∃x. P x ∧ R x) → (∃x. Q x ∧ R x)

Basic results

Inclusion

Theorem. incl_intro
(∀x. x ∈ A → x ∈ B) → A ⊆ B
Theorem. incl_elim
A ⊆ B → x ∈ A → x ∈ B
Theorem. incl_refl
A ⊆ A
Theorem. incl_trans
A ⊆ B → B ⊆ C → A ⊆ C
Theorem. incl_antisym
A ⊆ B → B ⊆ A → A = B
Theorem. incl_from_eq
A = B → A ⊆ B
Theorem. incl_from_eq_rev
A = B → B ⊆ A
Theorem. incl_ext
(∀X. X ⊆ A ↔ X ⊆ B) → A = B

Class comprehension

Theorem. comp_elim
u ∈ {x | P x} → P u
Theorem. comp_intro
set u → P u → u ∈ {x | P x}
Theorem. set_intro
x ∈ A → set x
Theorem. comp_intro_from
u ∈ A → P u → u ∈ {x | P x}
Theorem. sep_is_subclass
{x | x ∈ A ∧ P x} ⊆ A
Theorem. sep_is_set
set A → set {x | x ∈ A ∧ P x}

Binary operations on sets

Theorem. intersection_elim
x ∈ A ∩ B → x ∈ A ∧ x ∈ B
Theorem. intersection_eliml
x ∈ A ∩ B → x ∈ A
Theorem. intersection_elimr
x ∈ A ∩ B → x ∈ B
Theorem. intersection_intro
x ∈ A → x ∈ B → x ∈ A ∩ B
Theorem. union_intro
x ∈ A ∨ x ∈ B → x ∈ A ∪ B
Theorem. union_introl
x ∈ A → x ∈ A ∪ B
Theorem. union_intror
x ∈ B → x ∈ A ∪ B
Theorem. union_elim
x ∈ A ∪ B → x ∈ A ∨ x ∈ B
Theorem. intersection_incl_left
A ∩ B ⊆ A
Theorem. intersection_incl_right
A ∩ B ⊆ B
Theorem. union_incl_left
A ⊆ A ∪ B
Theorem. union_incl_right
B ⊆ A ∪ B
Theorem. intersection_from_incl
A ⊆ B → A ∩ B = A
Theorem. incl_from_intersection
A ∩ B = A → A ⊆ B
Theorem. union_from_incl
A ⊆ B → A ∪ B = B
Theorem. incl_from_union
A ∪ B = B → A ⊆ B
Theorem. intersection_idem
A ∩ A = A
Theorem. union_idem
A ∪ A = A
Theorem. intersection_comm
A ∩ B = B ∩ A
Theorem. union_comm
A ∪ B = B ∪ A
Theorem. intersection_distl
A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)
Theorem. intersection_distr
(A ∪ B) ∩ C = (A ∩ C) ∪ (B ∩ C)
Theorem. union_distl
A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)
Theorem. union_distr
(A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C)
Theorem. intersection_assocl
(A ∩ B) ∩ C = A ∩ (B ∩ C)
Theorem. intersection_assocr
A ∩ (B ∩ C) = (A ∩ B) ∩ C
Theorem. union_incl_in_union
A1 ⊆ B1 → A2 ⊆ B2 → A1 ∪ A2 ⊆ B1 ∪ B2
Theorem. union_incl_in
A1 ⊆ B → A2 ⊆ B → A1 ∪ A2 ⊆ B
Theorem. diff_intro
x ∈ A → ¬x ∈ B → x ∈ A \ B
Theorem. diff_elim
x ∈ A \ B → x ∈ A ∧ ¬x ∈ B
Theorem. diff_eliml
x ∈ A \ B → x ∈ A
Theorem. diff_elimr
x ∈ A \ B → ¬x ∈ B
Theorem. compl_intro
set x → ¬x ∈ A → x ∈ compl A
Theorem. compl_elim
x ∈ compl A → ¬x ∈ A
Theorem. diff_as_inter
A \ B = A ∩ compl B
Theorem. diff_incl
A \ B ⊆ A
Theorem. diff_dist_inter
(A ∩ B) \ C = (A \ C) ∩ (B \ C)

The empty set

Theorem. empty_contra
x ∈ ∅ → ⊥
Theorem. empty_efq
x ∈ ∅ → A
Theorem. empty_set_is_least
∅ ⊆ A
Theorem. empty_diff
A \ B = ∅ → A ⊆ B
Theorem. diff_disjoint
A ∩ B = ∅ → A \ B = A
Theorem. union_neutl
∅ ∪ A = A
Theorem. union_neutr
A ∪ ∅ = A
Theorem. disjoint_property
A ∩ B = ∅ → x ∈ A → x ∈ B → ⊥
Theorem. set_with_no_elements
(∀x. ¬x ∈ A) → A = ∅
Theorem. non_empty
¬A = ∅ → ∃x. x ∈ A
Theorem. non_empty_from_witness
x ∈ A → ¬A = ∅
Theorem. intersection_rel_compl
A ∩ (B \ A) = ∅

Operations on systems of sets

Theorem. Intersection_intro
set x → (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M
Theorem. Intersection_elim
x ∈ ⋂M → y ∈ M → x ∈ y
Theorem. Union_intro_ex
(∃y. y ∈ M ∧ x ∈ y) → x ∈ ⋃M
Theorem. Union_intro
y ∈ M → x ∈ y → x ∈ ⋃M
Theorem. Union_elim
x ∈ ⋃M → ∃y. y ∈ M ∧ x ∈ y
Theorem. Intersection_dec
A ⊆ B → ⋂B ⊆ ⋂A
Theorem. Union_inc
A ⊆ B → ⋃A ⊆ ⋃B
Theorem. Intersection_intro_witness
y ∈ M → (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M
Theorem. Intersection_intro_non_empty
¬M = ∅ → (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M
Theorem. Intersection_is_lower_bound
A = ⋂M → B ∈ M → A ⊆ B
Theorem. lower_bound_incl_in_Intersection
(∀x. x ∈ M → u ⊆ x) → u ⊆ ⋂M

The universal class and Russell's paradox

Theorem. UnivCl_intro
set x → x ∈ UnivCl
Theorem. UnivCl_elim
x ∈ UnivCl → set x
Theorem. UnivCl_is_greatest
A ⊆ UnivCl
Theorem. DiagCl_is_proper
¬set DiagCl
Theorem. UnivCl_is_proper
¬set UnivCl
Theorem. intersection_neutr
A ∩ UnivCl = A
Theorem. intersection_neutl
UnivCl ∩ A = A
Theorem. intersection_compl
A ∩ compl A = ∅
Theorem. union_compl
A ∪ compl A = UnivCl
Theorem. Intersection_empty_set
⋂∅ = UnivCl
Theorem. diff_union
(A \ B) ∪ B = A ∪ B
Theorem. diff_union_subclass
A ⊆ X → (X \ A) ∪ A = X

Singletons, pair sets and pairs

Theorem. sg_elim
set a → x ∈ {a} → x = a
Theorem. sg_intro
set a → x = a → x ∈ {a}
Theorem. sg_equi
set a → (x ∈ {a} ↔ x = a)
Theorem. sg_neg_intro
set y → ¬x = y → ¬x ∈ {y}
Theorem. sg_incl_in
x ∈ A → {x} ⊆ A
Theorem. Intersection_sg
set a → ⋂{a} = a
Theorem. sg_is_inj
set x → set y → {x} = {y} → x = y
Theorem. sg_of_proper_class
¬set A → {A} = UnivCl
Theorem. in21
set x → x ∈ {x, y}
Theorem. in22
set y → y ∈ {x, y}
Theorem. Intersection_pair_set
set x ∧ set y → ⋂{x, y} = x ∩ y
Theorem. Union_pair_set
set x ∧ set y → ⋃{x, y} = x ∪ y
Theorem. set_union
set x → set y → set (x ∪ y)
Theorem. set_sg
set x → set {x}
Theorem. set_pair
set x → set y → set (x, y)
Theorem. set_from_sg
set {x} → set x
Theorem. setl_from_union
set (A ∪ B) → set A
Theorem. setr_from_union
set (A ∪ B) → set B
Theorem. setl_from_pair
set (x, y) → set x
Theorem. setr_from_pair
set (x, y) → set y
Theorem. pair_fst_conj
set x ∧ set y → fst (x, y) = x
Theorem. pair_scd_conj
set x ∧ set y → scd (x, y) = y
Theorem. pair_fst
set x → set y → fst (x, y) = x
Theorem. pair_scd
set x → set y → scd (x, y) = y
Theorem. pair_property_conj
set x ∧ set y → (x, y) = (x', y') → x = x' ∧ y = y'
Theorem. pair_property
set x → set y → (x, y) = (x', y') → x = x' ∧ y = y'
Theorem. prod_intro
x ∈ X → y ∈ Y → (x, y) ∈ X × Y
Theorem. prod_elim
t ∈ X × Y → ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y)
Theorem. prod_elim_pair
(x, y) ∈ X × Y → x ∈ X ∧ y ∈ Y
Theorem. prod_elim_lemma
t ∈ X × Y → fst t ∈ X ∧ scd t ∈ Y
Theorem. prod_eliml
t ∈ X × Y → fst t ∈ X
Theorem. prod_elimr
t ∈ X × Y → scd t ∈ Y
Theorem. empty_set_is_set
set ∅
Theorem. zero_neq_one
¬∅ = {∅}
Theorem. disjoint_sg_from_neq
set a → set b → ¬a = b → {a} ∩ {b} = ∅
Theorem. disjoint_sg_from_new
set a → ¬a ∈ X → X ∩ {a} = ∅
Theorem. subsets_of_sg
set a → x ⊆ {a} → x = ∅ ∨ x = {a}

Operations on families of sets

Theorem. family_union_intro
set (A i) → i ∈ I → x ∈ A i → x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i}
Theorem. family_union_elim
x ∈ ⋃{B | ∃i. i ∈ I ∧ B = A i} → ∃i. i ∈ I ∧ x ∈ A i ∧ set (A i)

Relations

Relationhood

Theorem. relation_unfold
relation R → ∀t. t ∈ R → ∃x. ∃y. t = (x, y)
Theorem. relation_fold
(∀t. t ∈ R → ∃x. ∃y. t = (x, y)) → relation R
Theorem. relation_elim
relation R → t ∈ R → ∃x. ∃y. t = (x, y)
Theorem. relation_from_incl
R ⊆ X × Y → relation R
Theorem. relation_subclass
R ⊆ Q → relation Q → relation R
Theorem. relation_union
relation R → relation Q → relation (R ∪ Q)

Domains and ranges

Theorem. dom_intro
(x, y) ∈ R → x ∈ dom R
Theorem. dom_elim
x ∈ dom R → ∃y. (x, y) ∈ R
Theorem. dom_incl
R ⊆ X × Y → dom R ⊆ X
Theorem. rng_intro
(x, y) ∈ R → y ∈ rng R
Theorem. rng_elim
y ∈ rng R → ∃x. (x, y) ∈ R
Theorem. rng_subclass
R ⊆ Q → rng R ⊆ rng Q
Theorem. dom_of_subclass_prod
R ⊆ X × Y → dom R ⊆ X
Theorem. rng_of_subclass_prod
R ⊆ X × Y → rng R ⊆ Y
Theorem. relation_incl_prod
relation R → dom R ⊆ X → rng R ⊆ Y → R ⊆ X × Y
Theorem. dom_union
dom (R ∪ Q) = dom R ∪ dom Q
Theorem. rng_union
rng (R ∪ Q) = rng R ∪ rng Q

Images and inverse images

Theorem. img_intro
x ∈ A → (x, y) ∈ R → y ∈ img R A
Theorem. img_elim
y ∈ img R A → ∃x. x ∈ A ∧ (x, y) ∈ R
Theorem. inv_img_intro
y ∈ B → (x, y) ∈ R → x ∈ inv_img R B
Theorem. inv_img_elim
x ∈ inv_img R B → ∃y. y ∈ B ∧ (x, y) ∈ R
Theorem. img_dist_union
img R (A ∪ B) = img R A ∪ img R B
Theorem. img_dist_inter
img R (A ∩ B) ⊆ img R A ∩ img R B
Theorem. img_incl
A ⊆ B → img R A ⊆ img R B
Theorem. img_incl_in_rng
img R A ⊆ rng R
Theorem. img_of_dom_is_rng
img R (dom R) = rng R
Theorem. inv_img_dist_inter
inv_img R (A ∩ B) ⊆ inv_img R A ∩ inv_img R B
Theorem. inv_img_dist_union
inv_img R (A ∪ B) = inv_img R A ∪ inv_img R B
Theorem. inv_img_incl
A ⊆ B → inv_img R A ⊆ inv_img R B
Theorem. inv_img_incl_in_dom
inv_img R B ⊆ dom R
Theorem. img_union
img (R ∪ Q) A = img R A ∪ img Q A

Composition of relations

Theorem. composition_is_relation
relation (S ∘ R)
Theorem. composition_elimr
(a, c) ∈ S ∘ R → ∃y. (a, y) ∈ R
Theorem. composition_eliml
(a, c) ∈ S ∘ R → ∃y. (y, c) ∈ S
Theorem. composition_elim
(a, c) ∈ S ∘ R → ∃y. (a, y) ∈ R ∧ (y, c) ∈ S
Theorem. composition_intro
(a, b) ∈ R → (b, c) ∈ S → (a, c) ∈ S ∘ R
Theorem. dom_composition
dom (S ∘ R) ⊆ dom R
Theorem. rng_composition
rng (S ∘ R) ⊆ rng S
Theorem. img_composition
img (S ∘ R) A = img S (img R A)
Theorem. inv_img_composition
inv_img (S ∘ R) B = inv_img R (inv_img S B)

Special relations

Theorem. empty_relation
relation ∅
Theorem. dom_empty_set
dom ∅ = ∅
Theorem. rng_empty_set
rng ∅ = ∅
Theorem. sg_relation
set a → set b → relation {(a, b)}
Theorem. dom_sg
set a → set b → dom {(a, b)} = {a}
Theorem. rng_sg
set a → set b → rng {(a, b)} = {b}
Theorem. img_sg_sg
set a → set b → img {(a, b)} {a} = {b}
Theorem. img_sg_sg_neq
set a → set b → set x → ¬a = x → img {(a, b)} {x} = ∅

Functions

Functionhood

Theorem. function_unfold
function f → relation f ∧ (∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2)
Theorem. map_unfold
map f X Y → function f ∧ dom f = X ∧ rng f ⊆ Y
Theorem. function_intro
relation f → (∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2) → function f
Theorem. fn_is_rel
function f → relation f
Theorem. fn_unique_value
function f → (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2
Theorem. map_is_function
map f X Y → function f
Theorem. map_is_relation
map f X Y → relation f
Theorem. map_intro
function f → dom f = X → rng f ⊆ Y → map f X Y
Theorem. fn_is_map
function f → dom f = X → map f X UnivCl
Theorem. map_dom
map f X Y → dom f = X
Theorem. function_subclass
f ⊆ g → function g → function f
Theorem. function_union
function f → function g → dom f ∩ dom g = ∅ → function (f ∪ g)
Theorem. map_union
map f X1 Y1 → map g X2 Y2 → X1 ∩ X2 = ∅ → map (f ∪ g) (X1 ∪ X2) (Y1 ∪ Y2)
Theorem. map_union_eq_rngs
map f X1 Y → map g X2 Y → X1 ∩ X2 = ∅ → map (f ∪ g) (X1 ∪ X2) Y
Theorem. subclass_dom_from_ex_uniq
(∀x. x ∈ X → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f) → X ⊆ dom f
Theorem. map_rng_weaken
map f X Y → Y ⊆ Z → map f X Z
Theorem. map_incl_in_prod
map f X Y → f ⊆ X × Y

Function application

Theorem. sg_eq_from_uniq
set x → (∀y. x = y ↔ P y) → {x} = {y | P y}
Theorem. sg_eq_from_ex_uniq
(∃b. set b ∧ ∀y. b = y ↔ P y) → (∃b. set b ∧ {b} = {y | P y})
Theorem. fn_img_lemma
function f → x ∈ dom f → ∃y. set y ∧ {y} = {y | (x, y) ∈ f}
Theorem. app_intro_lemma
(∃y. set y ∧ {y} = {y | (x, y) ∈ f}) → (x, y) ∈ f → y = app f x
Theorem. app_elim_lemma
(∃y. set y ∧ {y} = {y | (x, y) ∈ f}) → y = app f x → (x, y) ∈ f
Theorem. app_intro
function f → (x, y) ∈ f → y = app f x
Theorem. app_elim
function f → x ∈ dom f → y = app f x → (x, y) ∈ f
Theorem. map_app_intro
map f X Y → (x, y) ∈ f → y = app f x
Theorem. map_app_elim
map f X Y → x ∈ X → y = app f x → (x, y) ∈ f
Theorem. map_extensionality_lemma
map f X Y → map g X Y → (∀x. x ∈ X → app f x = app g x) → f ⊆ g
Theorem. map_extensionality
map f X Y → map g X Y → (∀x. x ∈ X → app f x = app g x) → f = g
Theorem. fn_app_exists
function f → x ∈ dom f → ∃y. y ∈ rng f ∧ y = app f x
Theorem. map_app_exists
map f X Y → x ∈ X → ∃y. y ∈ Y ∧ y = app f x
Theorem. app_is_set
function f → x ∈ dom f → set (app f x)
Theorem. map_app_in_cod
map f X Y → x ∈ X → app f x ∈ Y
Theorem. map_app_is_set
map f X Y → x ∈ X → set (app f x)

Function composition

Theorem. fn_from_term_plain
f = {t | ∃x. t = (x, y x)} → function f
Theorem. fn_from_term
f = {t | ∃x. P x ∧ t = (x, y x)} → function f
Theorem. dom_from_term
f = {t | ∃x. x ∈ X ∧ t = (x, y x)} → (∀x. x ∈ X → set (y x)) → dom f = X
Theorem. rng_from_term
f = {t | ∃x. x ∈ X ∧ t = (x, y x)} → (∀x. x ∈ X → y x ∈ Y) → rng f ⊆ Y
Theorem. map_from_term
f = {t | ∃x. x ∈ X ∧ t = (x, y x)} → (∀x. x ∈ X → y x ∈ Y) → map f X Y
Theorem. map_from_term_app
f = {t | ∃x. x ∈ X ∧ t = (x, y x)} → (∀x. x ∈ X → y x ∈ Y) → x ∈ X → app f x = y x
Theorem. composition_is_map
map f X Y → map g Y Z → map (g ∘ f) X Z
Theorem. map_app_composition
map f X Y → map g Y Z → x ∈ X → app (g ∘ f) x = app g (app f x)

Restricted functions

Theorem. restr_is_subclass
restr f A ⊆ f
Theorem. restr_intro
(x, y) ∈ f → x ∈ A → (x, y) ∈ restr f A
Theorem. restr_is_function
function f → function (restr f A)
Theorem. dom_restr
dom (restr f A) = dom f ∩ A
Theorem. dom_restr_subclass
map f X Y → A ⊆ X → dom (restr f A) = A
Theorem. map_restr
map f X Y → A ⊆ X → map (restr f A) A Y
Theorem. app_restr
map f X Y → A ⊆ X → x ∈ A → app f x = app (restr f A) x
Theorem. fn_app_restr
function f → x ∈ dom f → x ∈ A → app f x = app (restr f A) x
Theorem. map_img_of_dom_is_rng
map f X Y → img f X = rng f
Theorem. map_rng_elim
map f X Y → y ∈ rng f → ∃x. x ∈ X ∧ y = app f x

Special functions

Theorem. empty_function
function ∅
Theorem. empty_map
map ∅ ∅ Y
Definition. id_eq
id X = {t | ∃x. x ∈ X ∧ t = (x, x)}
Theorem. id_is_map
map (id X) X X
Theorem. id_app
x ∈ X → app (id X) x = x
Theorem. id_img
A ⊆ X → img (id X) A = A
Theorem. id_neutl
map f X Y → id Y ∘ f = f
Theorem. id_neutr
map f X Y → f ∘ id X = f
Theorem. sg_function
set a → set b → function {(a, b)}
Theorem. sg_map
set a → b ∈ Y → map {(a, b)} {a} Y
Theorem. img_graph2
set x → set y → img {(∅, x), ({∅}, y)} {∅, {∅}} = {x, y}

Partly functional relations

Definition. fn_on_equi
fn_on f A ↔ relation f ∧ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f
Theorem. fn_on_intro
relation f → (∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f) → fn_on f A
Theorem. fn_on_intro_cod
relation f → (∀x. x ∈ A → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f) → fn_on f A
Theorem. relation_from_fn_on
fn_on f A → relation f
Theorem. ex_uniq_from_fn_on
fn_on f A → ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f
Theorem. fn_on_from_function
function f → A ⊆ dom f → fn_on f A
Theorem. fn_on_from_map
map f X Y → A ⊆ X → fn_on f A
Theorem. function_from_fn_on
fn_on f X → dom f ⊆ X → function f
Theorem. fn_on_app_intro
fn_on f A → x ∈ A → (x, y) ∈ f → y = app f x
Theorem. fn_on_app_elim
fn_on f A → x ∈ A → y = app f x → (x, y) ∈ f
Theorem. fn_on_extensionality
fn_on f A → fn_on g A → (∀x. x ∈ A → app f x = app g x) → restr f A = restr g A
Theorem. fn_on_char
A ⊆ dom f → (fn_on f A ↔ relation f ∧ function (restr f A))

Injections, surjections, bijections

Theorem. inj_is_map
inj f X Y → map f X Y
Theorem. inj_elim
inj f X Y → a ∈ X → b ∈ X → app f a = app f b → a = b
Theorem. inj_intro
map f X Y → (∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b) → inj f X Y
Theorem. sur_is_map
sur f X Y → map f X Y
Theorem. sur_elim
sur f X Y → rng f = Y
Theorem. sur_intro
map f X Y → Y ⊆ rng f → sur f X Y
Theorem. bij_is_map
bij f X Y → map f X Y
Theorem. bij_is_inj
bij f X Y → inj f X Y
Theorem. bij_is_sur
bij f X Y → sur f X Y
Theorem. bij_from_inj_sur
inj f X Y → sur f X Y → bij f X Y
Theorem. composition_inj_inj_is_inj
inj f X Y → inj g Y Z → inj (g ∘ f) X Z
Theorem. composition_sur_sur_is_sur
sur f X Y → sur g Y Z → sur (g ∘ f) X Z
Theorem. composition_bij_bij_is_bij
bij f X Y → bij g Y Z → bij (g ∘ f) X Z
Theorem. inj_from_left_inv
map f X Y → (∃g. map g Y X ∧ g ∘ f = id X) → inj f X Y

Choice functions

Theorem. choice_fn_unfold
choice_function f → function f ∧ ∀x. x ∈ dom f → app f x ∈ x
Theorem. choice_function_intro
function f → (∀x. x ∈ dom f → app f x ∈ x) → choice_function f
Theorem. restr_is_choice_fn
choice_function f → choice_function (restr f A)
Theorem. choice_on_class
∃f. choice_function f ∧ dom f = A \ {∅}
Theorem. Diaconescu_Goodman_Myhill_theorem
(∀M. ∃f. choice_function f ∧ dom f = M \ {∅}) → A ∨ ¬A

Power sets

Theorem. power_intro
set x → x ⊆ y → x ∈ power y
Theorem. power_elim
x ∈ power M → x ⊆ M
Theorem. prod_incl_in_power
A × B ⊆ power (power (A ∪ B))
Theorem. set_prod
set A → set B → set (A × B)
Theorem. sep_in_power
set X → {x | x ∈ X ∧ P x} ∈ power X
Theorem. power_empty_set
power ∅ = {∅}
Theorem. power_sg
set a → power {a} = {∅, {a}}
Theorem. sg_incl_in_power
set x → {x} ⊆ power x
Theorem. function_is_set
function f → set (dom f) → set f
Theorem. map_is_set
map f X Y → set X → set f
Theorem. map_is_set_dom_cod
map f X Y → set X → set Y → set f

Well-founded relations

Definition. wf_equi
wf R M ↔ ∀A. A ⊆ M → ¬A = ∅ → ∃y. y ∈ A ∧ ¬∃x. x ∈ A ∧ (x, y) ∈ R
Theorem. wf_unfold
wf R M → ∀A. A ⊆ M → ¬A = ∅ → ∃y. y ∈ A ∧ ¬∃x. x ∈ A ∧ (x, y) ∈ R
Theorem. wf_induction_set
wf R M → A ⊆ M → (∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A) → A = M
Theorem. wf_induction
wf R M → (∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → P y) → P x) → (∀x. x ∈ M → P x)
Theorem. wf_rec_unique
wf R X → dom R ⊆ X → map f X Y → map g X Y → (∀x. x ∈ X → app f x = φ x (restr f (inv_img R {x}))) → (∀x. x ∈ X → app g x = φ x (restr g (inv_img R {x}))) → f = g
Theorem. wf_rec_existence
set X → set Y → wf R X → dom R ⊆ X → (∀x. ∀g. φ x g ∈ Y) → ∃f. set f ∧ map f X Y ∧ ∀x. x ∈ X → app f x = φ x (restr f (inv_img R {x}))

The natural numbers as ordinals

Definition. onat_inductive_sets_eq
onat_inductive_sets = {A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A}
Definition. onat_eq
onat = ⋂onat_inductive_sets
Definition. succ_eq
succ n = n ∪ {n}
Theorem. onat_is_set
set onat
Theorem. succ_is_set
set n → set (succ n)
Theorem. zero_in_onat
∅ ∈ onat
Theorem. succ_in_onat
n ∈ onat → succ n ∈ onat
Theorem. onat_induction_sets
A ⊆ onat → ∅ ∈ A → (∀n. n ∈ A → succ n ∈ A) → A = onat
Theorem. onat_induction
P ∅ → (∀n. n ∈ onat → P n → P (succ n)) → (∀n. n ∈ onat → P n)

Closure operators

Definition. clop_equi
closure_operator H U ↔ set U ∧ map H (power U) (power U) ∧ (∀X. X ⊆ U → X ⊆ app H X) ∧ (∀X. ∀Y. X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y) ∧ (∀X. X ⊆ U → app H (app H X) ⊆ app H X)
Definition. closure_system_equi
closure_system M U ↔ M ⊆ power U ∧ U ∈ M ∧ ∀T. T ⊆ M → ¬T=∅ → ⋂T ∈ M
Theorem. clop_app_in_cod
closure_operator H U → X ⊆ U → app H X ⊆ U
Theorem. clop_extensivity
closure_operator H U → X ⊆ U → X ⊆ app H X
Theorem. clop_monotony
closure_operator H U → X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y
Theorem. clop_idem
closure_operator H U → X ⊆ U → app H (app H X) = app H X
Theorem. clop_from_closure_system
closure_system M U → H = {t | ∃X. X ∈ power U ∧ t = (X, ⋂{A | A ∈ M ∧ X ⊆ A})} → closure_operator H U

Grothendieck universes

Definition. univ_equi
univ U ↔ ∅ ∈ U ∧ (∀x. x ∈ U → x ⊆ U) ∧ (∀x. x ∈ U → power x ∈ U) ∧ (∀I. ∀x. I ∈ U → map x I U → ⋃(img x I) ∈ U)
Definition. least_univ_eq
least_univ A = ⋂{U | univ U ∧ A ∈ U}
Definition. Univ_eq
Univ = least_univ onat
Axiom. universes
set x → ∃U. set U ∧ univ U ∧ x ∈ U
Theorem. univ_contains_empty_set
univ U → ∅ ∈ U
Theorem. univ_trans
univ U → x ∈ U → x ⊆ U
Theorem. univ_closed_power
univ U → x ∈ U → power x ∈ U
Theorem. univ_closed_family_union
univ U → I ∈ U → map x I U → ⋃(img x I) ∈ U
Theorem. univ_closed_subset
univ U → y ⊆ x → x ∈ U → y ∈ U
Theorem. univ_closed_intersection
univ U → x ∈ U → x ∩ y ∈ U
Theorem. univ_closed_union
univ U → x ∈ U → y ∈ U → x ∪ y ∈ U
Theorem. univ_closed_sg
univ U → x ∈ U → {x} ∈ U
Theorem. univ_closed_pair_set
univ U → x ∈ U → y ∈ U → {x, y} ∈ U
Theorem. univ_closed_pair
univ U → x ∈ U → y ∈ U → (x, y) ∈ U
Theorem. univ_closed_sep
univ U → A ∈ U → {x | x ∈ A ∧ P x} ∈ U
Theorem. univ_closed_prod
univ U → A ∈ U → B ∈ U → A × B ∈ U
Theorem. univ_closed_Intersection
univ U → M ∈ U → ¬M = ∅ → ⋂M ∈ U
Theorem. univ_closed_Union
univ U → M ∈ U → ⋃M ∈ U
Theorem. least_univ_is_univ
set A → set (least_univ A) ∧ univ (least_univ A)
Theorem. Univ_is_set
set Univ
Theorem. Univ_is_univ
univ Univ

Cardinal numbers

Numerousities

Definition. num_eq_equi
num_eq X Y ↔ ∃f. bij f X Y
Definition. num_le_equi
num_le X Y ↔ ∃f. inj f X Y
Definition. num_lt_equi
num_lt X Y ↔ num_le X Y ∧ ¬∃f. sur f X Y
Definition. Map_eq
Map X Y = {f | map f X Y}
Definition. indicator_eq
χ A X = {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∪ {t | ∃x. x ∈ A ∧ t = (x, {∅})}
Theorem. num_eq_intro
(∃f. bij f X Y) → num_eq X Y
Theorem. num_le_intro
(∃f. inj f X Y) → num_le X Y
Theorem. num_lt_intro
num_le X Y → (¬∃f. sur f X Y) → num_lt X Y
Theorem. Map_intro
map f X Y → set X → f ∈ Map X Y
Theorem. Map_elim
f ∈ Map X Y → map f X Y
Theorem. indicator_is_map
A ⊆ X → map (χ A X) X {∅, {∅}}
Theorem. indicator_app_is_zero
A ⊆ X → x ∈ X \ A → app (χ A X) x = ∅
Theorem. indicator_app_is_one
A ⊆ X → x ∈ A → app (χ A X) x = {∅}
Theorem. from_indicator_app_is_one
A ⊆ X → x ∈ X → app (χ A X) x = {∅} → x ∈ A
Theorem. power_equinum_indicators
set X → num_eq (power X) (Map X {∅, {∅}})
Theorem. Cantor's_theorem
set X → num_lt X (power X)

Ordinal numbers

Transitive sets

Definition. transitive_equi
transitive x ↔ ∀u. u ∈ x → u ⊆ x
Theorem. transitive_elim
transitive x → u ∈ x → u ⊆ x
Theorem. transitive_intro
(∀u. u ∈ x → u ⊆ x) → transitive x
Theorem. transitive_closed_succ
set x → transitive x → transitive (x ∪ {x})
Theorem. transitive_closed_Intersection
(∀x. x ∈ M → transitive x) → transitive (⋂M)
Theorem. transitive_closed_Union
(∀x. x ∈ M → transitive x) → transitive (⋃M)
Theorem. transitive_closed_power
transitive x → transitive (power x)

Ordinal numbers

Definition. well_order_equi
well_order R M ↔ wf R M ∧ (∀x. ∀y. ∀z. (x, y) ∈ R → (y, z) ∈ R → (x, z) ∈ R) ∧ (∀x. ∀y. ¬(¬((x, y) ∈ R ↔ x = y) ↔ (y, x) ∈ R))
Definition. diag_rl_eq
diag_rl = {t | ∃x. ∃y. t = (x, y) ∧ x ∈ y}
Definition. On_eq
On = Univ ∩ {α | transitive α ∧ ∀x. x ∈ α → transitive x}
Definition. on_lt_equi
on_lt = {t | ∃α. ∃β. α ∈ On ∧ β ∈ On ∧ α ∈ β ∧ t = (α, β)}
Theorem. On_is_transitive
β ∈ On → β ⊆ On

Statistics 

  53 definitions
  16 axioms
 377 theorems
────────────────
 446 items total