Library

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)

Theorem. equi_trans_ll
(C ↔ A) → (C ↔ B) → (A ↔ B)

Theorem. equi_trans_rr
(A ↔ C) → (B ↔ C) → (A ↔ B)

De Morgan's laws

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

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

Theorem. contraposition_rev_ii
(¬A → ¬B → ¬C) → C → 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

Theorem. rsubj_tollens
(A ↔ B) → ¬A → ¬B

Congrunce laws of equivalence

Theorem. equi_cong_neg
(A ↔ A') → (¬A ↔ ¬A')

Theorem. equi_cong_conj
(A ↔ A') → (B ↔ B') → (A ∧ B ↔ A' ∧ B')

Theorem. equi_cong_disj
(A ↔ A') → (B ↔ B') → (A ∨ B ↔ A' ∨ B')

Theorem. equi_cong_subj
(A ↔ A') → (B ↔ B') → ((A → B) ↔ (A' → B'))

Theorem. equi_cong_bij
(A ↔ A') → (B ↔ B') → ((A ↔ B) ↔ (A' ↔ 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. eq_cong
x = y → f x = f y

Theorem. eq_cong_ii
x = a → y = b → f x y = f a b

Theorem. eq_trans
x = y → y = z → x = z

Theorem. eq_trans_ll
y = x → y = z → x = z

Theorem. eq_trans_rr
x = y → z = y → 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. P x ∧ ∀y. P y → x = y) → (∃x. ∀y. x = y ↔ P y)

Theorem. ex_uniq_set_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

Theorem. pred_restr
A ⊆ B → (x ∈ B → P x) → (x ∈ A → P x)

Theorem. pred_ii_restr
A ⊆ B → (x ∈ B → y ∈ B → P x y) → (x ∈ A → y ∈ A → P x y)

Theorem. pred_iii_restr
A ⊆ B → (x ∈ B → y ∈ B → z ∈ B → P x y z) → (x ∈ A → y ∈ A → z ∈ A → P x y z)

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. separation
u ∈ {x | x ∈ A ∧ P x} ↔ u ∈ A ∧ P u

Theorem. sep_is_subclass
{x | x ∈ A ∧ P x} ⊆ A

Theorem. sep_is_set
set A → set {x | x ∈ A ∧ P x}

Theorem. separation_is_unique
(∃B. ∀x. x ∈ B ↔ x ∈ A ∧ P x) → (∃C. ∀B. C = B ↔ ∀x. x ∈ B ↔ 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. incl_contraposition
A ⊆ B → X \ B ⊆ X \ A

Theorem. diff_dist_inter
(A ∩ B) \ C = (A \ C) ∩ (B \ C)

Theorem. diff_is_involution
A ⊆ X → X \ (X \ A) = A

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. Union_is_upper_bound
A = ⋃M → B ∈ M → B ⊆ A

Theorem. Intersection_is_infimum
(∀x. x ∈ M → u ⊆ x) → u ⊆ ⋂M

Theorem. Union_is_supremum
(∀x. x ∈ M → x ⊆ u) → ⋃M ⊆ u

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

Theorem. compl_as_diff
compl A = UnivCl \ A

Theorem. incl_contraposition_compl
A ⊆ B → compl B ⊆ compl A

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}

Theorem. diff_sg_contra
x ∈ A \ {x} → ⊥

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)

Conditional expressions

Definition. cond_eq
if A x y = ⋂{u | (A ∧ u = x) ∨ (¬A ∧ u = y)}

Theorem. cond_eql
set x → A → if A x y = x

Theorem. cond_eqr
set y → ¬A → if A x y = y

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. map_rng
map f X Y → rng f ⊆ Y

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. ∀y. z = y ↔ (x, y) ∈ f) → X ⊆ dom f

Theorem. subclass_dom_from_ex_uniq_in_cod
(∀x. x ∈ X → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f) → X ⊆ dom f

Theorem. map_from_ex_uniq
f ⊆ X × Y → (∀x. x ∈ X → ∃b. ∀y. b = y ↔ (x, y) ∈ f) → map f X Y

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. iota_intro
P u → (∃a. set a ∧ ∀x. a = x ↔ P x) → u = ⋂{x | P x}

Theorem. iota_elim
u = ⋂{x |P x} → (∃a. set a ∧ ∀x. a = x ↔ P x) → P u

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

Images and inverse images

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

Theorem. fn_inv_img_dist_inter
function f → inv_img f (A ∩ B) = inv_img f A ∩ inv_img f B

Theorem. restr_img_self
img f A ⊆ img (restr f A) A

Theorem. replacement
function f → A ⊆ dom f → set A → set (img f A)

Theorem. replacement_strong
function f → set A → set (img f A)

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. power_UnivCl
power UnivCl = UnivCl

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

Orders

General concepts

Definition. is_max_equi
is_max R y A ↔ y ∈ A ∧ ∀x. x ∈ A → R x y

Definition. is_min_equi
is_min R y A ↔ y ∈ A ∧ ∀x. x ∈ A → R y x

Definition. is_supremum_equi
is_supremum R M y A ↔ (∀x. x ∈ A → R x y) ∧ (∀b. b ∈ M → (∀x. x ∈ A → R x b) → R y b)

Definition. is_infimum_equi
is_infimum R M y A ↔ (∀x. x ∈ A → R y x) ∧ (∀b. b ∈ M → (∀x. x ∈ A → R b x) → R b y)

Partial orders

Definition. po_equi
partial_order R M ↔ (∀x. x ∈ M → R x x) ∧ (∀x. ∀y. x ∈ M → y ∈ M → R x y → R y x → x = y) ∧ (∀x. ∀y. ∀z. x ∈ M → y ∈ M → z ∈ M → R x y → R y z → R x z)

Theorem. po_refl
partial_order R M → x ∈ M → R x x

Theorem. po_antisym
partial_order R M → x ∈ M → y ∈ M → R x y → R y x → x = y

Theorem. po_trans
partial_order R M → x ∈ M → y ∈ M → z ∈ M → R x y → R y z → R x z

Power set lattice

Theorem. incl_Knaster_Tarski_least
set a → map f (power a) (power a) → (∀x. ∀y. y ⊆ a → x ⊆ y → app f x ⊆ app f y) → ∃u. u ⊆ a ∧ app f u = u ∧ (∀x. x ⊆ a → app f x = x → u ⊆ x)

Theorem. incl_Knaster_Tarski_greatest
set a → map f (power a) (power a) → (∀x. ∀y. y ⊆ a → x ⊆ y → app f x ⊆ app f y) → ∃u. u ⊆ a ∧ app f u = u ∧ (∀x. x ⊆ a → app f x = x → x ⊆ u)

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_eq
onat = ⋂{A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A}

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

Theorem. truncated_power_closed
univ U → x ∈ U → U ∩ power x ∈ U

Theorem. truncated_power_idem
univ U → U ∩ power U = U

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)

Theorem. Banach_decomposition_theorem
set X → rng g ⊆ X → ∃A. ∃B. img f A = B ∧ X \ A = img g (Y \ B)

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

The real numbers

Axiomatic definition

Declaration. real_decl
ℝ = _

Declaration. radd_decl
a + b = _

Declaration. rmul_decl
a⋅b = _

Declaration. rneg_decl
-a = _

Declaration. rinv_decl
/a = _

Definition. rsub_eq
a - b = a + (-b)

Definition. rdiv_eq
a/b = a⋅(/b)

Declaration. le_decl
x ≤ y ↔ _

Definition. lt_equi
a < b ↔ a ≤ b ∧ ¬a = b

Definition. upper_bound_equi
upper_bound b A ↔ ∀x. x ∈ A → x ≤ b

Definition. is_sup_equi
is_sup s A ↔ upper_bound s A ∧ (∀b. b ∈ ℝ → upper_bound b A → s ≤ b)

Axiom. real_is_set
set ℝ

Axiom. radd_closed
a ∈ ℝ → b ∈ ℝ → a + b ∈ ℝ

Axiom. rmul_closed
a ∈ ℝ → b ∈ ℝ → a⋅b ∈ ℝ

Axiom. rneg_closed
a ∈ ℝ → -a ∈ ℝ

Axiom. rinv_closed
a ∈ ℝ → ¬a = 0 → /a ∈ ℝ

Axiom. radd_comm
a ∈ ℝ → b ∈ ℝ → a + b = b + a

Axiom. rmul_comm
a ∈ ℝ → b ∈ ℝ → a⋅b = b⋅a

Axiom. radd_neutr
a ∈ ℝ → a + 0 = a

Axiom. radd_inv
a ∈ ℝ → a + (-a) = 0

Axiom. rmul_neutr
a ∈ ℝ → a⋅1 = a

Axiom. rmul_inv
a ∈ ℝ → ¬a = 0 → a⋅(/a) = 1

Axiom. radd_assoc
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a + b) + c = a + (b + c)

Axiom. rmul_assoc
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a⋅b)⋅c = a⋅(b⋅c)

Axiom. rmul_distl_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a⋅(b + c) = a⋅b + a⋅c

Axiom. rle_refl
a ∈ ℝ → a ≤ a

Axiom. rle_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → b ≤ c → a ≤ c

Axiom. rle_antisym
a ∈ ℝ → b ∈ ℝ → a ≤ b → b ≤ a → a = b

Axiom. rle_total
a ∈ ℝ → b ∈ ℝ → a ≤ b ∨ b ≤ a

Axiom. rle_compat_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → a + c ≤ b + c

Axiom. rle_compat_mul
a ∈ ℝ → b ∈ ℝ → 0 ≤ a → 0 ≤ b → 0 ≤ a⋅b

Axiom. lub_property
A ⊆ ℝ → ¬A = ∅ → (∃b. b ∈ ℝ ∧ upper_bound b A) → (∃s. s ∈ ℝ ∧ is_sup s A)

Basic results

Theorem. rsub_closed
a ∈ ℝ → b ∈ ℝ → a - b ∈ ℝ

Theorem. rdiv_closed
a ∈ ℝ → b ∈ ℝ → ¬b = 0 → a/b ∈ ℝ

Theorem. rreci_closed
a ∈ ℝ → ¬a = 0 → 1/a ∈ ℝ

Theorem. radd_neutl
a ∈ ℝ → 0 + a = a

Theorem. rmul_neutl
a ∈ ℝ → 1⋅a = a

Theorem. radd_cancel
a ∈ ℝ → b ∈ ℝ → a + b - b = a

Theorem. rsub_cancel
a ∈ ℝ → b ∈ ℝ → a - b + b = a

Theorem. radd_cancel_rr
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + c = b + c → a = b

Theorem. radd_cancel_ll
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → c + a = c + b → a = b

Theorem. radd_cancel_lr
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → c + a = b + c → a = b

Theorem. radd_cancel_rl
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + c = c + b → a = b

Theorem. rmul_distr_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a + b)⋅c = a⋅c + b⋅c

Theorem. rmul_rzero
a ∈ ℝ → a⋅0 = 0

Theorem. rmul_lzero
a ∈ ℝ → 0⋅a = 0

Theorem. rmul_compatr_neg
a ∈ ℝ → b ∈ ℝ → -(a⋅b) = a⋅(-b)

Theorem. rmul_compatl_neg
a ∈ ℝ → b ∈ ℝ → -(a⋅b) = (-a)⋅b

Theorem. rmul_distl_sub
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a⋅(b - c) = a⋅b - a⋅c

Theorem. rmul_distr_sub
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a - b)⋅c = a⋅c - b⋅c

Theorem. rsub_zero
a ∈ ℝ → a - 0 = a

Theorem. rsub_self
a ∈ ℝ → a - a = 0

Theorem. rsub_from_zero
a ∈ ℝ → 0 - a = -a

Theorem. rneg_involution
x ∈ ℝ → -(-x) = x

Theorem. rmul_minus_one
x ∈ ℝ → (-1)⋅x = -x

Theorem. rmul_cancel_neg
a ∈ ℝ → b ∈ ℝ → (-a)⋅(-b) = a⋅b

Theorem. rneg_dist_add
a ∈ ℝ → b ∈ ℝ → -(a + b) = -a + -b

Theorem. rsub_neg
a ∈ ℝ → b ∈ ℝ → -(a - b) = b - a

Theorem. rdiv_closed
a ∈ ℝ → b ∈ ℝ → ¬b = 0 → a/b ∈ ℝ

Theorem. rreci_closed
a ∈ ℝ → ¬a = 0 → 1/a ∈ ℝ

Theorem. rdiv_reci
a ∈ ℝ → ¬a = 0 → 1/a = /a

Theorem. rdiv_self
a ∈ ℝ → ¬a = 0 → a/a = 1

Theorem. rinv_one
1 = /1

Theorem. rdiv_neut
a ∈ ℝ → a/1 = a

Theorem. rmul_reci_cancel
a ∈ ℝ → ¬a = 0 → a⋅(1/a) = 1

Theorem. rreci_non_zero
a ∈ ℝ → ¬a = 0 → ¬1/a = 0

Theorem. rdiv_dist_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → ¬c = 0 → (a + b)/c = a/c + b/c

Theorem. rdiv_dist_sub
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → ¬c = 0 → (a - b)/c = a/c - b/c

Theorem. rsq_non_zero
a ∈ ℝ → ¬a = 0 → ¬a⋅a = 0

Theorem. rsq_is_zero_impl
a ∈ ℝ → a⋅a = 0 → a = 0

Theorem. rmul_non_zero
a ∈ ℝ → b ∈ ℝ → ¬a = 0 → ¬b = 0 → ¬a⋅b = 0

Theorem. zero_product_property
a ∈ ℝ → b ∈ ℝ → a⋅b = 0 → a = 0 ∨ b = 0

Useful lemmata

Theorem. rmul_expand_add_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ → (a + b)⋅(c + d) = a⋅c + b⋅c + a⋅d + b⋅d

Theorem. radd_assoc_llloolo
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c + d = a + (b + c) + d

Theorem. radd_assoc_llloloo
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ → a + b + c + d = a + (b + c + d)

Theorem. radd_assoc_llllooo
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ → a + b + c + d = a + (b + (c + d))

Theorem. radd_assoc_llolloo
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ → a + b + c + d = (a + b) + (c + d)

Theorem. radd_perm_213
a ∈ ℝ → b ∈ ℝ → a + b + c = b + a + c

Theorem. radd_perm_132
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = a + c + b

Theorem. radd_perm_231
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = b + c + a

Theorem. radd_perm_312
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = c + a + b

Theorem. radd_perm_321
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = c + b + a

Theorem. radd_perm_1423
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ → a + b + c + d = a + d + b + c

Theorem. rsub_cancel_middle
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a - b) + (b - c) = a - c

Basic inequalities

Theorem. le_eq_trans
a ≤ b → b = c → a ≤ c

Theorem. eq_le_trans
a = b → b ≤ c → a ≤ c

Theorem. neq_from_lt
a < b → ¬a = b

Theorem. le_from_lt
a < b → a ≤ b

Theorem. lt_intro
a ≤ b → ¬a = b → a < b

Theorem. rle_neg
a ∈ ℝ → b ∈ ℝ → ¬a ≤ b → b ≤ a

Theorem. rle_compat_addl
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → c + a ≤ c + b

Theorem. rle_compat_sub
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → a - c ≤ b - c

Theorem. rle_add
a ∈ ℝ → b ∈ ℝ → a' ∈ ℝ → b' ∈ ℝ → a ≤ a' → b ≤ b' → a + b ≤ a' + b'

Theorem. rneg_non_negative
x ∈ ℝ → 0 ≤ x → -x ≤ 0

Theorem. rle_neg_swaps
a ∈ ℝ → b ∈ ℝ → a ≤ b → -b ≤ -a

Theorem. rmul_nn_np
a ∈ ℝ → b ∈ ℝ → 0 ≤ a → b ≤ 0 → a⋅b ≤ 0

Theorem. rmul_np_nn
a ∈ ℝ → b ∈ ℝ → a ≤ 0 → 0 ≤ b → a⋅b ≤ 0

Theorem. rmul_np_np
a ∈ ℝ → b ∈ ℝ → a ≤ 0 → b ≤ 0 → 0 ≤ a⋅b

Theorem. rle_lt_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → b < c → a < c

Theorem. rlt_lt_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a < b → b < c → a < c

Theorem. rlt_compat_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a < b → a + c < b + c

Theorem. rlt_compat_sub
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a < b → a - c < b - c

Theorem. rlt_add_cancel_rr
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + c < b + c → a < b

Theorem. rle_lt_tricho
a ∈ ℝ → b ∈ ℝ → a ≤ b ∨ b < a

Theorem. rsq_is_non_negative
a ∈ ℝ → 0 ≤ a⋅a

Theorem. rsq_is_positive
a ∈ ℝ → ¬a = 0 → 0 < a⋅a

Theorem. rle_as_diff
a ∈ ℝ → b ∈ ℝ → a ≤ b → 0 ≤ b - a

Theorem. rle_from_diff
a ∈ ℝ → b ∈ ℝ → 0 ≤ b - a → a ≤ b

Theorem. rle_compat_mulr
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → 0 ≤ c → a⋅c ≤ b⋅c

Theorem. rle_compat_mull
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → 0 ≤ c → c⋅a ≤ c⋅b

Theorem. rreci_positive
a ∈ ℝ → 0 < a → 0 < 1/a

Absolute value

Definition. abs_eq
abs x = if (0 ≤ x) x (-x)

Theorem. rabs_eql
x ∈ ℝ → 0 ≤ x → abs x = x

Theorem. rabs_eqr
x ∈ ℝ → ¬0 ≤ x → abs x = -x

Theorem. rabs_non_positive
x ∈ ℝ → x ≤ 0 → abs x = -x

Theorem. rabs_closed
x ∈ ℝ → abs x ∈ ℝ

Theorem. rabs_bounded
a ∈ ℝ → x ∈ ℝ → -a ≤ x → x ≤ a → abs x ≤ a

Theorem. rabs_ge_arg
x ∈ ℝ → x ≤ abs x

Theorem. rabs_ge_neg_arg
x ∈ ℝ → -x ≤ abs x

Theorem. rabs_symm
x ∈ ℝ → abs (-x) = abs x

Theorem. rabs_triangle_ineq
x ∈ ℝ → y ∈ ℝ → abs (x + y) ≤ abs x + abs y

Theorem. rabs_dist_mul
x ∈ ℝ → y ∈ ℝ → abs (x⋅y) = (abs x)⋅(abs y)

The natural numbers

Basic results

Definition. nat_eq
ℕ = ⋂{A | A ⊆ ℝ ∧ 0 ∈ A ∧ ∀n. n ∈ A → n + 1 ∈ A}

Theorem. nat_incl_in_real
ℕ ⊆ ℝ

Theorem. nat_is_set
set ℕ

Theorem. zero_in_nat
0 ∈ ℕ

Theorem. succ_in_nat
n ∈ ℕ → n + 1 ∈ ℕ

Theorem. nat_induction_sets
A ⊆ ℕ → 0 ∈ A → (∀n. n ∈ A → n + 1 ∈ A) → A = ℕ

Theorem. nat_induction
P 0 → (∀n. n ∈ ℕ → P n → P (n + 1)) → (∀n. n ∈ ℕ → P n)

Theorem. nat_non_negative
n ∈ ℕ → 0 ≤ n

Theorem. nat_succ_non_zero
n ∈ ℕ → ¬(n + 1 = 0)

Theorem. nat_succ_inj
a ∈ ℕ → b ∈ ℕ → a + 1 = b + 1 → a = b

Theorem. nat_rec_uniqueness
app f 0 = x0 ∧ (∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)) → app g 0 = x0 ∧ (∀n. n ∈ ℕ → app g (n + 1) = φ n (app g n)) → ∀n. n ∈ ℕ → app f n = app g n

Theorem. nat_rec_existence
set X → x0 ∈ X → (∀n. n ∈ ℕ → ∀x. x ∈ X → φ n x ∈ X) → ∃f. set f ∧ (map f ℕ X ∧ (app f 0 = x0 ∧ ∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)))

Theorem. nat_recursion
set X → x0 ∈ X → (∀n. n ∈ ℕ → ∀x. x ∈ X → φ n x ∈ X) → ∃g. set g ∧ ∀f. g = f ↔ map f ℕ X ∧ (app f 0 = x0 ∧ ∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n))

Theorem. nadd_neutl
a ∈ ℕ → 0 + a = a

Theorem. nadd_neutr
a ∈ ℕ → a + 0 = a

Theorem. nsub_zero
a ∈ ℕ → a - 0 = a

Theorem. nmul_neutl
a ∈ ℕ → 1⋅a = a

Theorem. nmul_neutr
a ∈ ℕ → a⋅1 = a

Theorem. nmul_lzero
a ∈ ℕ → 0⋅a = 0

Theorem. nmul_rzero
a ∈ ℕ → a⋅0 = 0

Theorem. nadd_comm
a ∈ ℕ → b ∈ ℕ → a + b = b + a

Theorem. nmul_comm
a ∈ ℕ → b ∈ ℕ → a⋅b = b⋅a

Theorem. nadd_assoc
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a + b) + c = a + (b + c)

Theorem. nmul_distl_add
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a⋅(b + c) = a⋅b + a⋅c

Theorem. nmul_distr_add
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a + b)⋅c = a⋅c + b⋅c

Theorem. nmul_distl_sub
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a⋅(b - c) = a⋅b - a⋅c

Theorem. nmul_distr_sub
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a - b)⋅c = a⋅c - b⋅c

Theorem. nmul_compatl_neg
a ∈ ℕ → b ∈ ℕ → -(a⋅b) = (-a)⋅b

Theorem. nmul_compatr_neg
a ∈ ℕ → b ∈ ℕ → -(a⋅b) = a⋅(-b)

Theorem. nadd_closed
a ∈ ℕ → b ∈ ℕ → a + b ∈ ℕ

Theorem. nmul_closed
a ∈ ℕ → b ∈ ℕ → a⋅b ∈ ℕ

Theorem. nat_zero_or_succ
n ∈ ℕ → n = 0 ∨ ∃m. m ∈ ℕ ∧ n = m + 1

Theorem. nat_non_zero_is_succ
n ∈ ℕ → ¬n = 0 → ∃m. m ∈ ℕ ∧ n = m + 1

Basic inequalities

Theorem. nle_refl
a ∈ ℕ → a ≤ a

Theorem. nle_antisym
a ∈ ℕ → b ∈ ℕ → a ≤ b → b ≤ a → a = b

Theorem. nle_trans
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → b ≤ c → a ≤ c

Theorem. nle_total
a ∈ ℕ → b ∈ ℕ → a ≤ b ∨ b ≤ a

Theorem. nle_compat_addl
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → c + a ≤ c + b

Theorem. nle_compat_add
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → a + c ≤ b + c

Theorem. nle_lt_trans
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → b < c → a < c

Theorem. nlt_lt_trans
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a < b → b < c → a < c

Theorem. nlt_add_cancel_rr
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a + c < b + c → a < b

Theorem. nle_lt_tricho
a ∈ ℕ → b ∈ ℕ → a ≤ b ∨ b < a

Theorem. nat_succ_le_from_lt
n ∈ ℕ → k ∈ ℕ → n < k → n + 1 ≤ k

Theorem. nle_succ_split
k ∈ ℕ → n ∈ ℕ → k ≤ n + 1 → k ≤ n ∨ k = n + 1

Strong induction

Theorem. nat_strong_induction
P 0 → (∀n. n ∈ ℕ → (∀k. k ∈ ℕ → k ≤ n → P k) → P (n + 1)) → (∀n. n ∈ ℕ → P n)

The integers

Basic results

Definition. int_eq
ℤ = {z | z ∈ ℝ ∧ ∃a. ∃b. a ∈ ℕ ∧ b ∈ ℕ ∧ z = a - b}

Theorem. int_incl_in_real
ℤ ⊆ ℝ

Theorem. nat_incl_in_int
ℕ ⊆ ℤ

Theorem. ineg_closed
a ∈ ℤ → -a ∈ ℤ

Theorem. iadd_closed
a ∈ ℤ → b ∈ ℤ → a + b ∈ ℤ

Theorem. isub_closed
a ∈ ℤ → b ∈ ℤ → a - b ∈ ℤ

Theorem. imul_closed
a ∈ ℤ → b ∈ ℤ → a⋅b ∈ ℤ

Theorem. iadd_neutl
a ∈ ℤ → 0 + a = a

Theorem. iadd_neutr
a ∈ ℤ → a + 0 = a

Theorem. isub_zero
a ∈ ℤ → a - 0 = a

Theorem. isub_self
a ∈ ℤ → a - a = 0

Theorem. imul_neutl
a ∈ ℤ → 1⋅a = a

Theorem. imul_neutr
a ∈ ℤ → a⋅1 = a

Theorem. imul_lzero
a ∈ ℤ → 0⋅a = 0

Theorem. imul_rzero
a ∈ ℤ → a⋅0 = 0

Theorem. iadd_comm
a ∈ ℤ → b ∈ ℤ → a + b = b + a

Theorem. imul_comm
a ∈ ℤ → b ∈ ℤ → a⋅b = b⋅a

Theorem. iadd_assoc
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a + b) + c = a + (b + c)

Theorem. imul_distl_add
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a⋅(b + c) = a⋅b + a⋅c

Theorem. imul_distr_add
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a + b)⋅c = a⋅c + b⋅c

Theorem. imul_distl_sub
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a⋅(b - c) = a⋅b - a⋅c

Theorem. imul_distr_sub
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a - b)⋅c = a⋅c - b⋅c

Theorem. imul_compatl_neg
a ∈ ℤ → b ∈ ℤ → -(a⋅b) = (-a)⋅b

Theorem. imul_compatr_neg
a ∈ ℤ → b ∈ ℤ → -(a⋅b) = a⋅(-b)

Theorem. isub_neg
a ∈ ℤ → b ∈ ℤ → -(a - b) = b - a

Theorem. isub_cancel_middle
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a - b) + (b - c) = a - c

Basic inequalities

Theorem. ile_refl
a ∈ ℤ → a ≤ a

Theorem. ile_antisym
a ∈ ℤ → b ∈ ℤ → a ≤ b → b ≤ a → a = b

Theorem. ile_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → b ≤ c → a ≤ c

Theorem. ile_total
a ∈ ℤ → b ∈ ℤ → a ≤ b ∨ b ≤ a

Theorem. ile_compat_addl
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → c + a ≤ c + b

Theorem. ile_compat_add
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → a + c ≤ b + c

Theorem. ile_lt_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → b < c → a < c

Theorem. ilt_lt_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a < b → b < c → a < c

Theorem. ilt_add_cancel_rr
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a + c < b + c → a < b

Theorem. ile_lt_tricho
a ∈ ℤ → b ∈ ℤ → a ≤ b ∨ b < a

Elementary number theory

Definition. divides_equi
divides m a ↔ ∃k. k ∈ ℤ ∧ a = m⋅k

Definition. cong_equi
cong a b m ↔ divides m (a - b)

Definition. divisors_eq
divisors a = {d | d ∈ ℕ ∧ divides d a}

Definition. prime_equi
prime a ↔ 2 ≤ a ∧ divisors a = {1, a}

Theorem. cong_intro
k ∈ ℤ → a - b = m⋅k → cong a b m

Theorem. cong_elim
cong a b m → ∃k. k ∈ ℤ ∧ (a - b) = m⋅k

Theorem. cong_refl
a ∈ ℤ → m ∈ ℤ → cong a a m

Theorem. cong_symm
a ∈ ℤ → b ∈ ℤ → m ∈ ℤ → cong a b m → cong b a m

Theorem. cong_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → m ∈ ℤ → cong a b m → cong b c m → cong a c m

Formal theorems and proofs

Table of contents

Morse-Kelley set theory

Definitions

Axioms

Classical logic

Inference rules

Propositional logic

The relationship of EFQ, LEM, DNE

Useful theorems

De Morgan's laws

Projections

Congrunce laws of equivalence

First order logic

Bounded quantification

De Morgan's laws

First order logic with equality

Useful theorems

Unique existence

Basic results

Inclusion

Class comprehension

Binary operations on sets

The empty set

Operations on systems of sets

The universal class and Russell's paradox

Singletons, pair sets and pairs

Operations on families of sets

Conditional expressions

Relations

Relationhood

Domains and ranges

Images and inverse images

Composition of relations

Special relations

Functions

Functionhood

Function application

Function composition

Restricted functions

Images and inverse images

Special functions

Partly functional relations

Injections, surjections, bijections

Choice functions

Power sets

Orders

General concepts

Partial orders

Power set lattice

Well-founded relations

The natural numbers as ordinals

Closure operators

Grothendieck universes

Cardinal numbers

Numerousities

Ordinal numbers

Transitive sets

Ordinal numbers

The real numbers

Axiomatic definition

Basic results

Useful lemmata

Basic inequalities

Absolute value

The natural numbers

Basic results

Basic inequalities

Strong induction

The integers

Basic results

Basic inequalities

Elementary number theory