Set Theory

3

Axioms 3.1

27module set.axioms

The set of axioms we will be using for our set theory is called the Zermelo-Fraenkel axioms with Choice, abbreviated ZFC. There are other systems of axioms we could use, but ZFC is a commonly accepted set.

You may be hoping that $\in$ will come with two axioms, an introduction and an elimination rule. Sadly this is not the case.

We do get an elimination rule. It says that two sets are equal if they contain exactly the same elements. This is traditionally known as extensionality.

11axiom zfc.extensionality :
12    |- ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b
13end

We will be presenting the axioms as unschematized statements in first-order logic without using the iota operator. This is done to make clear the distinction between the axioms for which this can be done, and those for which it can't. We will state more natural forms of these axioms as theorems later.

Intuitively, a set is supposed to be a collection of all the objects with a certain property. Therefore, we might naturally expect to have an introduction rule similar to the following:

 axiom zfc.comprehension [p(_) : sentence(term)] :
    |- ∃x, ∀y, (y ∈ x ↔ p(y))
 end

However, such an axiom would be inconsistent. In particular, we would run into Russell's paradox: the axiom allows us to construct the set $X = \{x ~|~ x \not\in x\}$ which consists of all sets which do not contain themselves. Then we ask if $X \in X$. If it is then it should not be and if it isn't then it should be. We have a contradiction.

This leads us to the conclusion that not all properties can define sets. The remainder of the axioms of ZFC essentially define restricted forms of our idealized comprehension axiom which are believed not to lead to a contradiction. This will leave us with various operations which we can use to define our sets. In the end, almost all the sets we care about will be definable with these operations and so we will be able to act much as if we did have unrestricted comprehension.

The empty set axiom asserts the existence of a set with no elements.

46axiom zfc.empty_set :
47    |- ∃x, ∀y, y ∉ x 
48end

For any two sets we can form the set containing exactly those two sets.

52axiom zfc.pairing :
53    |- ∀a, ∀b, ∃x, ∀y, y ∈ x ↔ y = a ∨ y = b
54end

For any set we can take the union of all elements in the set.

58axiom zfc.union :
59    |- ∀a, ∃x, ∀y, y ∈ x ↔ (∃z, y ∈ z ∧ z ∈ a)
60end

For any set we can form the set of all subsets of the set (the powerset).

64axiom zfc.powerset :
65    |- ∀a, ∃x, ∀y, y ∈ x ↔ (∀z, z ∈ y → z ∈ a)
66end

There is a set containing the empty set with the property that for any $x$ in the set, the set also contains $x \cup \{x\}$. Such a set is called an inductive set and must be infinite. Without this axiom we would have no way to prove any infinite sets exist.

73axiom zfc.infinity :
74    |- ∃x, (∃y, y ∈ x ∧ ∀z, z ∉ y) 
75         ∧ (∀y, y ∈ x → ∃z, z ∈ x ∧ (∀w, w ∈ z ↔ w ∈ y ∨ w = y))
76end

Then we get the two axiom schemas. These are statements about all sentences which can't be stated using only quantifiers. The first says that for any set we can take the subset of all elements with a particular property. This is quite similar to the rejected comprehension axiom, but this one doesn't lead to contradictions (as far as we know). This is sometimes also called separation or restricted comprehension.

85axiom zfc.specification [p(_) : sentence(term)] :
86    |- ∀a, ∃x, ∀y, y ∈ x ↔ y ∈ a ∧ p(y)
87end

This axiom asserts that the image of any set under a function (implicitly defined by $p$) exists. This is surprisingly rarely required.

92axiom zfc.replacement [p(_0, _1) : sentence(term, term)] :
93    |- ∀a, (∀x, x ∈ a → ∃!y, p(x, y)) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ p(z, y)))
94end

The final axiom has a formal statement that is somewhat difficult to parse. But the important point is that it guarantees that we do not get an infinite chain of descending sets $x_0 \ni x_1 \ni x_2 \ni \dots$. In other words, all sets are nested at a finite depth (despite the fact that some sets contain an infinite number of elements).

102axiom zfc.regularity :
103    |- ∀a, (∃x, x ∈ a) → (∃y, y ∈ a ∧ ¬∃z, (z ∈ y ∧ z ∈ a))
104end

The final axiom is the famed Axiom of Choice. It is the C in ZFC. However it has a much longer first order statement and it is generally considered more polite to be clear when one is using it. So we will postpone adding it until it becomes necessary.

Set Operations 3.2

30module set.operations

The fundamental operation over sets is forming the set of all elements with a certain property. We discussed previously that this set does not always exist, however the iota operator allows us to define notation for it which will have the expected properties if it does exist.

6notation comprehension
7    term ::= "{" x:@binding(term) " | " sentence(x) "}"
8end

10definition
11    {x | p(x)} := ℩y, ∀x, x ∈ y ↔ p(x)
12end

We want to prove that if the set $\{x ~|~ p(x)\}$ exists, then the notation we have given for it will refer to that set. We need to invoke the iota axiom from the previous chapter.

18theorem uncomp.def [p(_) : sentence(term)] : (∃x, ∀y, y ∈ x ↔ p(y))
19    |- ∀y, y ∈ {x | p(x)} ↔ p(y) 
20proof
21    -- this property is essentially the definition of {x | p(x)} so we just
22    -- need to extract it using iota.unique. to do this we need that
23    -- the set is unique.
24    suffices ∃!x, ∀y, y ∈ x ↔ p(y) by iota.unique [∀y, y ∈ _ ↔ p(y)];
25
26    -- we can unwrap the definition of ∃!. this step is by definition.
27    suffices (∃x, ∀y, y ∈ x ↔ p(y)) ∧ (∃*x, ∀y, y ∈ x ↔ p(y));
28
29    -- we already have the lhs as a hypothesis.
30    suffices ∃*x, ∀y, y ∈ x ↔ p(y) by and.intro [∃x, ∀y, y ∈ x ↔ p(y)] [∃*x, ∀y, y ∈ x ↔ p(y)];
31
32    -- now we unwrap the definition of ∃*.
33    suffices ∀a, ∀b, (∀y, y ∈ a ↔ p(y)) ∧ (∀y, y ∈ b ↔ p(y)) → a = b;
34
35    -- let's extract all the pieces of this definition.
36    arbitrary a;
37    arbitrary b;
38    assume (∀y, y ∈ a ↔ p(y)) ∧ (∀y, y ∈ b ↔ p(y));
39    thus ∀y, y ∈ a ↔ p(y) by and.elim_left  [∀y, y ∈ a ↔ p(y)] [∀y, y ∈ b ↔ p(y)];
40    thus ∀y, y ∈ b ↔ p(y) by and.elim_right [∀y, y ∈ a ↔ p(y)] [∀y, y ∈ b ↔ p(y)];
41
42    -- now we can prove the equality using extensionality.
43    suffices ∀x, x ∈ a ↔ x ∈ b as
44        follows ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b by zfc.extensionality;
45        thus ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b specializing ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b;
46        thus (∀x, x ∈ a ↔ x ∈ b) → a = b     specializing ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b;
47        thus a = b by modus_ponens [∀x, x ∈ a ↔ x ∈ b] [a = b];
48    ;
49
50    arbitrary x;
51
52    -- We can use the transitivity of ↔ to finish the proof.
53    follows x ∈ a ↔ p(x) specializing ∀y, y ∈ a ↔ p(y);
54    follows x ∈ b ↔ p(x) specializing ∀y, y ∈ b ↔ p(y);
55    thus p(x) ↔ x ∈ b  by iff.symm [x ∈ b] [p(x)];
56    thus x ∈ a ↔ x ∈ b by iff.trans [x ∈ a] [p(x)] [x ∈ b];
57qed

Sorry, was that painful to read? It was painful to write. That proof wasn't actually very complicated but it was 40 lines long anyway. This is not sustainable. Lucky we have something to help. Vampire is an automated theorem prover. It will find proofs of mathematical facts automatically. We can make a new tactic that sends the current known facts and goal to Vampire to have it generate a proof. This proof is then translated for Watson to understand. This is a very complex but also very powerful tactic which eliminates the need for tedious manipulations.

68tactic justification.logically
69    justification ::= @kw"logically"
70end

At this point we are also going to start doing more complex mathematics so it will helpful to add a few more useful tactics.

Sometimes it is helpful to annotate exactly which hypotheses go into an application of a theorem. We will add given as a justification which uses Vampire like logically but also checks that Vampire uses the given hypotheses.

79grammar_category sentence_list

81tactic sentence_list.one sentence_list ::= sentence:@fragment(sentence) end

82tactic sentence_list.many sentence_list ::= sentence:@fragment(sentence) @kw"and" rest:sentence_list end

84grammar_category givens

86tactic givens.none givens ::= end

87tactic givens.some givens ::= @kw"given" sentences:sentence_list end

89tactic justification.given
90    justification ::= @kw"given" givens:sentence_list
91end

We will also extend the by tactic to use Vampire to apply the provided theorem. Note that Vampire can't do second order reasoning so this won't work with any theorems that contain templates more complex than unparameterized terms.

97grammar_category theorem_list

99tactic theorem_list.one theorem_list ::= thm:@name end

100tactic theorem_list.many theorem_list ::= thm:@name "," rest:theorem_list end

102tactic justification.by.vampire
103    -- bind stronger than the original to override it.
104    justification (600) ::= @kw"by" thms:theorem_list givens:givens
105end

107tactic justification.by_def
108    justification ::= @kw"by_def" sentence:@fragment(sentence)
109end

If we want to have Vampire use a theorem multiple times the recall tactic will add the statement of the theorem to the current proof state, making it so Vampire can use it in all future proofs.

115tactic tactic.recall
116    tactic ::= @kw"recall" thm:@name ";" next:tactic
117end

We will also add the done tactic which is just an alias for using a justification to prove the current goal instead of a tactic. This is equivalent to thus goal <just>.

123tactic tactic.done
124    tactic ::= @kw"done" just:justification
125end

We will also add a cases tactic. This is a little more complex then just splitting an or. By default, Vampire is used to prove this disjunction of all the case conditions. Or a separate justification can be provided for this purpose. Then the provided tactics are used to prove each case implies the original goal.

133grammar_category case_list

134grammar_category case

136tactic case_list.one  case_list ::= c:case end

137tactic case_list.many case_list ::= c:case rest:case_list end

139tactic case
140    case ::= "|" sentence:@fragment(sentence) @kw"then" tactic:tactic
141end

143tactic tactic.cases
144    tactic ::= @kw"cases" just:justification ":" cases:case_list
145end

The final new tactic we will add is the let tactic. This allows making new definitions inside a proof. These definitions will be invisible to Vampire so adding them won't effect reasoning at all.

151tactic tactic.let
152    tactic ::= @kw"let" name:@name ":=" frag:@fragment(term) ";" next:tactic
153end

The Subset Relation

The other fundamental relationship between sets, besides equality, is the subset relation.

161notation subset
162    sentence (500) ::= term " ⊆ " term
163end

165definition
166    a ⊆ b := ∀x, x ∈ a → x ∈ b
167end

169theorem sub.def [a b : term] :
170    |- a ⊆ b ↔ ∀x, x ∈ a → x ∈ b
171proof
172    done by iff.refl [a ⊆ b]
173qed

The subset relation is both reflexive and transitive.

177theorem sub.refl [a : term] :
178    |- a ⊆ a
179proof
180    suffices ∀x, x ∈ a → x ∈ a by sub.def;
181    done logically
182qed

184theorem sub.trans [a b c : term] : (a ⊆ b) (b ⊆ c)
185    |- a ⊆ c
186proof
187    follows ∀x, x ∈ a → x ∈ b by sub.def given a ⊆ b;
188    follows ∀x, x ∈ b → x ∈ c by sub.def given b ⊆ c;
189    thus    ∀x, x ∈ a → x ∈ c logically;
190    done by sub.def
191qed

We also have that if two sets are subsets of each other then they are equal. In fact, this is just a restatement of the extensionality axiom.

196theorem sub.sub_eq [a b : term] : (a ⊆ b) (b ⊆ a)
197    |- a = b
198proof
199    follows ∀x, x ∈ a → x ∈ b by sub.def given a ⊆ b;
200    follows ∀x, x ∈ b → x ∈ a by sub.def given b ⊆ a;
201    thus ∀x, x ∈ a ↔ x ∈ b logically;
202    thus a = b by zfc.extensionality;
203qed

We can also have the notion of a strict subset.

207notation strict_subset
208    sentence (500) ::= term " ⊂ " term
209end

211@[reducible]
212definition
213    a ⊂ b := a ⊆ b ∧ a ≠ b
214end

216theorem ssub.def [a b : term] :
217    |- a ⊂ b ↔ (a ⊆ b ∧ a ≠ b)
218proof
219    done by iff.refl [a ⊂ b]
220qed

Bounded Quantifiers

When defining the subset relation we wrote $\forall x, x \in a \to x \in b$. The $x \in a \to$ component makes the quantifier only meaningful for elements of the set $a$. This is a very common pattern so we will define shorthand notation for it.

229notation forall.bounded
230    sentence (000) ::= "∀" x:@binding(term) " ∈ " term ", " sentence(x)
231end

233@[reducible]
234definition
235    ∀x ∈ X, p(x) := ∀x, x ∈ X → p(x)
236end

Note that for the existential quantifier we use $\land$ instead of $\to$ because we are looking for an element that is both in the set and satisfies the property.

242notation exists.bounded
243    sentence (000) ::= "∃" x:@binding(term) " ∈ " term ", " sentence(x)
244end

246@[reducible]
247definition
248    ∃x ∈ X, p(x) := ∃x, x ∈ X ∧ p(x)
249end

The Empty Set

Returning to mathematics, we can use the unrestricted comprehension syntax to define our first concrete set, the empty set.

256notation empty_set
257    term ::= "∅"
258end

260definition
261    ∅ := {x | ⊥}
262end

The empty set axiom tells us that this set actually exists.

266theorem empty.def :
267    |- ∀x, x ∉ ∅
268proof
269    -- expand the definition of ∅
270    suffices ∀x, x ∉ {x | ⊥};
271    -- existence from the axiom
272    follows ∃x, ∀y,  y ∉ x        by zfc.empty_set;
273    thus    ∃x, ∀y, (y ∈ x ↔ ⊥)   logically;     
274    -- and then set comprehension is always unique
275    thus    ∀y, (y ∈ {x | ⊥} ↔ ⊥) by uncomp.def [⊥];
276    thus    ∀y,  y ∉ {x | ⊥}      logically;
277qed

We can also characterize a non-empty set as one containing an element.

281theorem nonempty.has_element [a : term] :
282    |- a ≠ ∅ ↔ ∃x, x ∈ a
283proof
284    follows ∀x, x ∉ ∅          by empty.def;
285    follows a = ∅ ↔  ∀x, x ∉ a by zfc.extensionality; 
286    thus    a ≠ ∅ ↔ ¬∀x, x ∉ a logically;
287    thus    a ≠ ∅ ↔  ∃x, x ∈ a logically;
288qed

The empty set is a subset of any set.

292theorem empty.is_sub [a : term] :
293    |- ∅ ⊆ a
294proof
295    follows ∀x, x ∉ ∅         by empty.def;
296    thus    ∀x, x ∈ ∅ → x ∈ a logically;
297qed

Every subset of the empty set is the empty set.

301theorem empty.sub_is_empty [a : term] : (a ⊆ ∅)
302    |- a = ∅
303proof
304    follows ∀x, x ∈ a → x ∈ ∅ by sub.def;
305    follows ∀x,         x ∉ ∅ by empty.def;
306    thus   ¬∃x, x ∈ a         logically;
307    thus    a = ∅             by zfc.extensionality;
308qed

The Unordered Pair

We can develop the pair set in an essentially identical way.

314notation pair
315    term ::= "{" term ", " term "}"
316end

318definition 
319    {a, b} := {x | x = a ∨ x = b}
320end

This time it is the pairing axiom that tells us that this set exists.

324theorem pair.def [a b : term] :
325    |- ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b)
326proof
327    suffices ∀x, x ∈ {y | y = a ∨ y = b} ↔ (x = a ∨ x = b);
328    follows ∃c, ∀x, x ∈ c ↔ (x = a ∨ x = b)               by zfc.pairing;
329    thus    ∀x, x ∈ {y | y = a ∨ y = b} ↔ (x = a ∨ x = b) by uncomp.def [_ = a ∨ _ = b];
330qed

The unordered pair is unordered. That is, it is symmetric.

334theorem pair.symm [a b : term] :
335    |- {a, b} = {b, a}
336proof
337    thus ∀x, x ∈ {a, b} ↔ x ∈ {b, a} by pair.def;
338    thus {a, b} = {b, a}             by zfc.extensionality;
339qed

The unordered pair being a subset is equivalent to both elements of the pair being members of the set.

344theorem pair.sub [a b A : term] :
345    |- (a ∈ A ∧ b ∈ A) ↔ {a, b} ⊆ A
346proof
347    done by sub.def, pair.def
348qed

It is also non-empty.

352theorem pair.non_empty [a b : term] :
353    |- {a, b} ≠ ∅
354proof
355    follows a ∈ {a, b} by pair.def;
356    thus {a, b} ≠ ∅    by empty.def;
357qed

The Singleton Set

We can define the singleton set as the pair of the same element twice. We could define it as simply $\{a\} = \{x ~|~ x = a\}$ but how would we prove this set exists? We would have to appeal to the pairing axiom anyway.

365notation singleton
366    term ::= "{" term "}"
367end

369definition
370    {a} := {a, a}
371end

373theorem singleton.def [a : term] :
374    |- ∀x, x ∈ {a} ↔ x = a
375proof
376    suffices ∀x, x ∈ {a, a} ↔ x = a;
377    thus ∀x, x ∈ {a, a} ↔ x = a by pair.def;
378qed

An element being in a set is equivalent to the singleton set being a subset.

382theorem singleton.sub [a A : term] :
383    |- a ∈ A ↔ {a} ⊆ A
384proof
385    follows a ∈ A → (∀x, x ∈ {a} → x ∈ A) by singleton.def;
386    follows (∀x, x ∈ {a} → x ∈ A) → a ∈ A by singleton.def;
387    done by sub.def
388qed

Restricted Comprehension

In contrast to unrestricted comprehensions, which are not always sets, a comprehension which is limited to be a subset of another set always exists. This is guaranteed by the specification axiom.

396notation restricted_comprehension
397    term ::= "{" x:@binding(term) " ∈ " term " | " sentence(x) "}"
398end

400definition
401    {x ∈ X | p(x)} := {x | x ∈ X ∧ p(x)}
402end

This proof follows from the specification axiom.

406theorem comp.def [p(_) : sentence(term)] [X : term] :
407    |- ∀y, y ∈ {x ∈ X | p(x)} ↔ (y ∈ X ∧ p(y))
408proof
409    suffices ∀y, y ∈ {x | x ∈ X ∧ p(x)} ↔ (y ∈ X ∧ p(y));
410    hence ∀a, ∃x, ∀y, y ∈ x ↔ (y ∈ a ∧ p(y)) by zfc.specification [p(_)];
411    follows ∃x, ∀y, y ∈ x ↔ (y ∈ X ∧ p(y))   logically;
412    thus ∀y, y ∈ {x | x ∈ X ∧ p(x)} ↔ (y ∈ X ∧ p(y)) by uncomp.def [_ ∈ X ∧ p(_)];
413qed

It easily follows from this definition that a restricted comprehension is always a subset of the original set.

418theorem comp.sub [p(_) : sentence(term)] [X : term] :
419    |- {x ∈ X | p(x)} ⊆ X
420proof
421    follows ∀y, y ∈ {x ∈ X | p(x)} ↔ (y ∈ X ∧ p(y)) by comp.def [p(_)] [X];
422    thus    ∀y, y ∈ {x ∈ X | p(x)} →  y ∈ X         logically;
423qed

Because comp.def is a second order theorem, that is it is schematized over all predicates $p$, Vampire cannot reason with it automatically. This is why we had to manually provide the template instantiations when we invoked it. Restricted comprehension comes up so frequently and invoking second order theorems is so tedious that we are just going to hard code this theorem so that it is automatically given to Vampire any time a comprehension appears in the local context.

The Set Map

TODO

437notation term.with_term
438    term (1000) ::= @name "(" term ")"
439end

441notation set_map
442  term ::= "{" term(x) " | " x:@binding(term) " ∈ " term "}"
443end

445definition
446    {f(x) | x ∈ A} := {y | ∃x, x ∈ A ∧ y = f(x)}
447end

The proof follows from the replacement axiom and the definition of the set map.

451theorem set_map.def [f(_) : term(term)] [A : term] :
452    |- ∀y, y ∈ {f(x) | x ∈ A} ↔ (∃x, x ∈ A ∧ y = f(x))
453proof
454    suffices ∀y, y ∈ {z | ∃x, x ∈ A ∧ z = f(x)} ↔ (∃x, x ∈ A ∧ y = f(x));
455    suffices (∃x, ∀y, y ∈ x ↔ ∃x, x ∈ A ∧ y = f(x)) by uncomp.def [∃x, x ∈ A ∧ _ = f(x)];
456    hence ∀x ∈ A, ∃!y, y = f(x) logically;
457    follows ∀a, (∀x, x ∈ a → ∃!y, y = f(x)) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ y = f(z))) by zfc.replacement [_1 = f(_0)];
458    done logically
459qed

Unions

We can return to defining new sets with the union of a set.

465notation big_union
466    term (000) ::= "⋃" term
467end

469definition
470    ⋃a := {x | ∃y, x ∈ y ∧ y ∈ a}
471end

Once more the existence of this set is guaranteed by the union axiom of ZFC.

475theorem big_union.def [a : term] :
476    |- ∀x, x ∈ ⋃a ↔ (∃y, x ∈ y ∧ y ∈ a)
477proof
478    suffices ∀x, x ∈ {x | ∃y, x ∈ y ∧ y ∈ a} ↔ (∃y, x ∈ y ∧ y ∈ a);
479    follows ∃x, ∀y, y ∈ x ↔ (∃z, y ∈ z ∧ z ∈ a) by zfc.union;
480    follows ∀x, x ∈ {x | ∃y, x ∈ y ∧ y ∈ a} ↔ (∃y, x ∈ y ∧ y ∈ a) by uncomp.def [∃y, _ ∈ y ∧ y ∈ a];
481qed

Any element of a set is a subset of the union of that set.

485theorem big_union.super [a b : term] : (a ∈ b)
486    |- a ⊆ ⋃b
487proof
488    follows ∀x, (∃y, x ∈ y ∧ y ∈ b) ↔ x ∈ ⋃b by big_union.def;
489    thus    ∀x,      x ∈ a          → x ∈ ⋃b logically;
490qed

Next, we show that the union of a singleton is the element of the singleton.

494theorem big_union.singleton [a : term] :
495    |- ⋃{a} = a
496proof
497    follows ∀x, x ∈ {a} ↔ x = a by singleton.def;
498    hence ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ y ∧ y ∈ {a}) by big_union.def [{a}];
499    thus ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ y ∧ y = a) logically;
500    follows ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ a) logically;
501    follows ∀x, x ∈ ⋃{a} ↔ x ∈ a logically;
502    done by zfc.extensionality
503qed

We can define the regular union using the pair and the big union. Once again, although we could define this directly using unrestricted comprehension, it is easier to do it this way to avoid repeated proofs of existence.

508notation union
509    term (650>) ::= term " ∪ " term
510end

512definition
513    a ∪ b := ⋃{a, b}
514end

The definition of the union can be easily proved from the definitions of the big union and the pair.

519theorem union.def [a b : term] :
520    |- ∀x, x ∈ a ∪ b ↔ (x ∈ a ∨ x ∈ b)
521proof
522    suffices ∀x, x ∈ ⋃{a, b} ↔ (x ∈ a ∨ x ∈ b);
523    follows  ∀x, x ∈ ⋃{a, b} ↔ ∃y, x ∈ y ∧ y ∈ {a, b} by big_union.def;
524    follows  ∀y, y ∈  {a, b} ↔ (y = a ∨ y = b)        by pair.def;
525    done logically
526qed

The union operator is also symmetric. This follows either from the fact that the unordered pair is symmetric, or just the symmetry of or itself.

531theorem union.symm [a b : term] :
532    |- a ∪ b = b ∪ a
533proof
534    follows ∀x, x ∈ a ∪ b ↔ (x ∈ a ∨ x ∈ b) by union.def;
535    follows ∀x, x ∈ b ∪ a ↔ (x ∈ a ∨ x ∈ b) by union.def;
536    thus a ∪ b = b ∪ a                      by zfc.extensionality;
537qed

The union is also associative. This follows from the associativity of or.

541theorem union.assoc [a b c : term] :
542    |- a ∪ (b ∪ c) = (a ∪ b) ∪ c
543proof
544    follows ∀x, x ∈ a ∪ (b ∪ c) ↔ (x ∈ a ∨ (x ∈ b ∨ x ∈ c)) by union.def;
545    follows ∀x, x ∈ (a ∪ b) ∪ c ↔ ((x ∈ a ∨ x ∈ b) ∨ x ∈ c) by union.def;
546    thus a ∪ (b ∪ c) = (a ∪ b) ∪ c                          by zfc.extensionality;
547qed

Either set in the union is a subset of the union as a whole. These facts are really just simplifications of the defining fact.

552theorem union.left_sub [a b : term] :
553    |- a ⊆ a ∪ b
554proof
555    follows ∀x, (x ∈ a ∨ x ∈ b) ↔ x ∈ a ∪ b by union.def;
556    thus    ∀x,  x ∈ a          → x ∈ a ∪ b logically;
557qed

559theorem union.right_sub [a b : term] :
560    |- b ⊆ a ∪ b
561proof
562    follows ∀x, (x ∈ a ∨ x ∈ b) ↔ x ∈ a ∪ b by union.def;
563    thus    ∀x,          x ∈ b  → x ∈ a ∪ b logically;
564qed

Intersections

Instead of defining the big intersection with an unrestricted comprehension as we did for the big union, we will define it as a subset of the union. This makes it easier to prove existence.

572notation big_inter
573    term (000) ::= "⋂" term
574end

576definition
577    ⋂a := {x ∈ ⋃a | ∀y, y ∈ a → x ∈ y}
578end

This definition implies that the intersection of the empty set is the empty set. However, based on the defining property of the intersection, the intersection of the empty set should be the proper class of all sets, which isn't a set. So we restrict the definition theorem to only applying to non-empty sets.

585theorem big_inter.def [a : term] : (a ≠ ∅)
586    |- ∀x, x ∈ ⋂a ↔ (∀y, y ∈ a → x ∈ y)
587proof
588    arbitrary x;
589    suffices x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} ↔ (∀y, y ∈ a → x ∈ y);
590
591    assume x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} then ∀y, y ∈ a → x ∈ y logically;
592
593    assume ∀y, y ∈ a → x ∈ y then x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} as
594        obtain y st y ∈ a  by nonempty.has_element;
595        follows     x ∈ y  logically;
596        thus        x ∈ ⋃a by big_union.def;
597        done logically
598    ;
599
600    done logically
601qed

The big intersection of a set is a subset of every element of the set.

605theorem big_inter.sub [a b : term] : (a ∈ b)
606    |- ⋂b ⊆ a
607proof
608    follows b ≠ ∅                            by nonempty.has_element;
609    follows ∀x, x ∈ ⋂b ↔ (∀y, y ∈ b → x ∈ y) by big_inter.def;
610    thus    ∀x, x ∈ ⋂b →              x ∈ a  logically;
611qed

We define the small intersection the same way we defined the small union.

615notation inter
616    term (700) ::= term " ∩ " term
617end

619definition
620    a ∩ b := ⋂{a, b}
621end

Since the pair set is always non-empty, the small intersection is always well defined.

626theorem inter.def [a b : term] :
627    |- ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b)
628proof
629    suffices ∀x, x ∈ ⋂{a, b} ↔ (x ∈ a ∧ x ∈ b);
630
631    -- we need that the pair set isn't empty to apply big_inter.def.
632    follows {a, b} ≠ ∅ by pair.non_empty; 
633    follows ∀x, x ∈ ⋂{a, b} ↔ (∀y, y ∈ {a, b} → x ∈ y) by big_inter.def;
634    follows ∀y, y ∈  {a, b} ↔ (y = a ∨ y = b)          by pair.def;
635    thus    ∀x, x ∈ ⋂{a, b} ↔ (x ∈ a ∧ x ∈ b)          logically;
636qed

Like the union, the intersection is symmetric and associative. The proofs are identical to those for union, just replacing every $\lor$ with an $\land$.

641theorem inter.symm [a b : term] :
642    |- a ∩ b = b ∩ a
643proof
644    follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
645    follows ∀x, x ∈ b ∩ a ↔ (x ∈ a ∧ x ∈ b) by inter.def;
646    thus a ∩ b = b ∩ a                      by zfc.extensionality;
647qed

649theorem inter.assoc [a b c : term] :
650    |- a ∩ (b ∩ c) = (a ∩ b) ∩ c
651proof
652    follows ∀x, x ∈ a ∩ (b ∩ c) ↔ (x ∈ a ∧ (x ∈ b ∧ x ∈ c)) by inter.def;
653    follows ∀x, x ∈ (a ∩ b) ∩ c ↔ ((x ∈ a ∧ x ∈ b) ∧ x ∈ c) by inter.def;
654    thus a ∩ (b ∩ c) = (a ∩ b) ∩ c                          by zfc.extensionality;
655qed

The intersection of two sets is a subset of both of the original sets.

659theorem inter.sub_left [a b : term] :
660    |- a ∩ b ⊆ a
661proof
662    follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
663    thus    ∀x, x ∈ a ∩ b →  x ∈ a          logically;
664qed

666theorem inter.sub_right [a b : term] :
667    |- a ∩ b ⊆ b
668proof
669    follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
670    thus    ∀x, x ∈ a ∩ b →          x ∈ b  logically;
671qed

673theorem inter.left_sub [a b c : term] : (c ⊆ a ∩ b)
674    |- c ⊆ a
675proof
676    follows ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def given c ⊆ a ∩ b;
677    follows ∀x, x ∈ c → x ∈ a         logically;
678qed

680theorem inter.right_sub [a b c : term] : (c ⊆ a ∩ b)
681    |- c ⊆ b
682proof
683    follows ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def given c ⊆ a ∩ b;
684    follows ∀x, x ∈ c →         x ∈ b logically;
685qed

687theorem inter.both_sub [a b c : term] : (a ⊆ c) (b ⊆ c)
688    |- a ∩ b ⊆ c
689proof
690    suffices ∀x, x ∈ a ∧ x ∈ b → x ∈ c by inter.def, sub.def;
691    follows  ∀x, x ∈ a         → x ∈ c by sub.def given a ⊆ c;
692    follows  ∀x,         x ∈ b → x ∈ c by sub.def given b ⊆ c;
693    done logically
694qed

696theorem inter.sub_both [a b c : term] : (c ⊆ a) (c ⊆ b)
697    |- c ⊆ a ∩ b
698proof
699    suffices ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def;
700    follows  ∀x, x ∈ c → x ∈ a         by sub.def given c ⊆ a;
701    follows  ∀x, x ∈ c →         x ∈ b by sub.def given c ⊆ b;
702    done logically
703qed

The Set Difference

We define the difference between two sets as the set of elements of the first set which are not in the second set.

709notation set_difference
710    term (700) ::= term " - " term
711end

713definition
714    a - b := {x ∈ a | x ∉ b}
715end

Since we used a restricted comprehension, the defining property follows directly without any more existence proofs.

720theorem set_diff.def [a b : term] :
721    |- ∀x, x ∈ a - b ↔ (x ∈ a ∧ x ∉ b)
722proof
723    suffices ∀x, x ∈ {y ∈ a | y ∉ b} ↔ (x ∈ a ∧ x ∉ b);
724    -- remember we gave Vampire the power to understand restricted comprehensions.
725    done logically 
726qed

The set difference is a subset of the first set. This follows from the fact that all restricted comprehensions are subsets.

731theorem set_diff.sub [a b : term] :
732    |- a - b ⊆ a
733proof
734    suffices {x ∈ a | x ∉ b} ⊆ a;
735    done by comp.sub [_ ∉ b] [a]
736qed

We can also characterize a non-empty difference.

740theorem set_diff.non_empty [a b : term] : (b ⊆ a)
741    |- a - b ≠ ∅ ↔ a ≠ b
742proof
743    assume a - b ≠ ∅ then a ≠ b as
744        obtain x st x ∈ a - b by nonempty.has_element;
745        thus x ∈ a ∧ x ∉ b    by set_diff.def;
746        thus a ≠ b            by zfc.extensionality;
747    ;
748
749    assume a ≠ b then a - b ≠ ∅ as
750        obtain x st (x ∈ a ∧ x ∉ b) ∨ (x ∈ b ∧ x ∉ a) by zfc.extensionality;
751        follows ¬(x ∈ b ∧ x ∉ a) by sub.def;
752        thus      x ∈ a ∧ x ∉ b  logically;
753        thus      x ∈ a - b      by set_diff.def;
754        thus      a - b ≠ ∅      by nonempty.has_element;
755    ;
756
757    done logically
758qed

The Powerset

We will define the powerset as the set of all subsets of a set.

764definition
765    𝒫(a) := {x | x ⊆ a}
766end

The existence of this set is provided by one of the ZFC axioms in the same manner as before.

771theorem powset.def [a : term] :
772    |- ∀x, x ∈ 𝒫(a) ↔ x ⊆ a
773proof
774    suffices ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a;
775    follows ∃b, ∀x, x ∈ b ↔ (∀y, y ∈ x → y ∈ a) by zfc.powerset;
776    thus    ∃b, ∀x, x ∈ b ↔ x ⊆ a;
777    thus    ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a by uncomp.def [_ ⊆ a];
778qed

The singletons and pairs of elements from the original set are both examples of sets in the powerset.

783theorem powset.singleton_in [a A : term] : (a ∈ A)
784    |- {a} ∈ 𝒫(A)
785proof
786    follows {a} ⊆ A by singleton.sub;
787    thus {a} ∈ 𝒫(A) by powset.def;
788qed

790theorem powset.pair_in [a b A : term] : (a ∈ A) (b ∈ A)
791    |- {a, b} ∈ 𝒫(A)
792proof
793    follows {a, b} ⊆ A by pair.sub;
794    thus {a, b} ∈ 𝒫(A) by powset.def;
795qed

If

Using restricted comprehensions we can define the if then else operator. This will be useful for casewise definitions.

802notation if
803    term ::= "if " sentence " then " term " else " term
804end

806definition
807    if p then a else b := {x ∈ a | p} ∪ {x ∈ b | ¬p}
808end

810theorem union.empty [a : term] :
811    |- a ∪ ∅ = a
812proof
813    todo
814qed

816theorem empty.union [a : term] :
817    |- ∅ ∪ a = a
818proof
819    done by union.empty, union.symm
820qed

822theorem if.true [p : sentence] [a b : term] : (p)
823    |- if p then a else b = a
824proof
825    suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = a;
826    follows {x ∈ a |  p} = a given p;
827    follows {x ∈ b | ¬p} = ∅ by empty.def given p;
828    follows a ∪ ∅ = a        by union.empty;
829    done logically
830qed

832theorem if.false [p : sentence] [a b : term] : (¬p)
833    |- if p then a else b = b
834proof
835    suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = b;
836    follows {x ∈ a |  p} = ∅ by empty.def given ¬p;
837    follows {x ∈ b | ¬p} = b given ¬p;
838    follows ∅ ∪ b = b        by empty.union;
839    done logically
840qed

842theorem if.swap [p : sentence] [a b : term] :
843    |- if p then a else b = if ¬p then b else a
844proof
845    cases:
846    | p  then
847        follows if  p then a else b = a by if.true [p] [a] [b];
848        follows ¬¬p logically; -- TODO: use vampire for this.
849        follows if ¬p then b else a = a by if.false [¬p] [b] [a];
850        done logically
851    | ¬p then
852        follows if  p then a else b = b by if.false [p] [a] [b];
853        follows if ¬p then b else a = b by if.true [¬p] [b] [a];
854        done logically
855qed

Functions 3.3

33module set.fn

The Ordered Pair

An ordered pair (a, b) is a set composed of a singleton {a} and a pair {a, b}. We can use ordered pairs to enforce certain structure on sets.

4notation ordered_pair
5    term ::= "⟨" term ", " term "⟩"
6end

8definition
9    ⟨a, b⟩ := {{a}, {a, b}}
10end

The proof follows from the pairing axiom and the definition of the ordered pair.

15theorem opair.def [a b : term] :
16    |- ∀x, x ∈ ⟨a, b⟩ ↔ (x = {a} ∨ x = {a, b})
17proof
18    suffices ∀x, x ∈ {{a}, {a, b}} ↔ (x = {a} ∨ x = {a, b});
19    follows ∃c, ∀x, x ∈ c ↔ (x = {a} ∨ x = {a, b})      by zfc.pairing;
20    thus ∀x, x ∈ {{a}, {a, b}} ↔ (x = {a} ∨ x = {a, b}) by uncomp.def [_ = {a} ∨ _ = {a, b}];
21qed

23theorem opair.unfold [a b : term] :
24    |- ⟨a, b⟩ = {{a}, {a, b}}
25proof
26    done by eq.refl [⟨a, b⟩]
27qed

Lets prove some basic properties of ordered pairs

31theorem opair.union [a b : term] :
32    |- ⋃⟨a, b⟩ = {a, b}
33proof
34    suffices ⋃{{a}, {a, b}} = {a, b};
35    thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
36    thus ∀x, x ∈ ⋃{{a}, {a, b}} ↔ (x ∈ {a} ∨ x ∈ {a, b}) by union.def [{a}] [{a, b}];
37    hence ∀x, (x = a ∨ (x = a ∨ x = b)) ↔ (x = a ∨ x = b) logically;
38    follows ∀x, (x ∈ {a} ∨ x ∈ {a, b}) ↔ (x = a ∨ (x = a ∨ x = b)) by singleton.def, pair.def;
39    done by zfc.extensionality
40qed

42theorem opair.inter [a b : term] :
43    |- ⋂⟨a, b⟩ = {a}
44proof
45    suffices ⋂{{a}, {a, b}} = {a};
46    thus ∀x, x ∈ {a} ↔ x = a by singleton.def;
47    thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
48    thus ∀x, x ∈ ⋂{{a}, {a, b}} ↔ (x ∈ {a} ∧ x ∈ {a, b}) by inter.def [{a}] [{a, b}];
49    hence ∀x, (x = a ∧ (x = a ∨ x = b)) ↔ x = a logically;
50    thus ∀x, x ∈ ⋂{{a}, {a, b}} ↔ x ∈ {a} by singleton.def;
51    follows ⋂{{a}, {a, b}} = {a} by zfc.extensionality;
52qed

Next, we define a function which gives us the first element of an ordered pair. We define this function somewhat broadly, but it allows for an easy proof.

56definition
57    π₁(a) := ⋃⋂a
58end

The proof follows from the definition of the ordered pair and many of the intersection properties we've shown.

62theorem opair_first.def [a b : term] :
63    |- π₁(⟨a, b⟩) = a
64proof
65    hence ⋂⟨a, b⟩ = {a} by opair.inter;
66    thus ⋃{a} = a by big_union.singleton;
67    hence ⋃⋂⟨a, b⟩ = a logically;
68qed

Naturally, we now define the second element of an ordered pair.

72definition
73    π₂(a) := ⋃{x ∈ ⋃a | ⋃a ≠ ⋂a → x ∉ ⋂a}
74end

This proof follows simply from the definition of the ordered pair and the properties of unions and intersections.

78theorem opair_second.def [a b : term] :
79    |- π₂(⟨a, b⟩) = b
80proof
81    suffices ⋃{x ∈ ⋃⟨a, b⟩ | ⋃⟨a, b⟩ ≠ ⋂⟨a, b⟩ → x ∉ ⋂⟨a, b⟩} = b;
82    follows ⋃⟨a, b⟩ = {a, b} by opair.union;
83    follows ⋂⟨a, b⟩ = {a}    by opair.inter;
84    -- We can simplify our goal with our known facts for the union and intersection
85    hence ⋃{x ∈ ⋃⟨a, b⟩ | ⋃⟨a, b⟩ ≠ ⋂⟨a, b⟩ → x ∉ ⋂⟨a, b⟩}
86        = ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} logically;
87    thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
88    follows ∀x, x ∈ {a} ↔ x = a by singleton.def;
89    follows {a, b} ≠ {a} ↔ a ≠ b logically;
90    hence ∀x, ((x = a ∨ x = b) ∧ (a ≠ b → x ∉ {a})) ↔ x = b logically;
91    thus ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x = b by zfc.extensionality;
92    hence ∀x, x = b ↔ x ∈ {b} by singleton.def;
93    follows ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x ∈ {b} logically;
94    follows {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = {b} by zfc.extensionality;
95    -- so π₂(⟨a, b⟩) = ⋃{b} = b
96    hence ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = ⋃{b} logically;
97    done by big_union.singleton
98qed

Finally, we show that two ordered pairs are equal iff their first and second elements are equal.

102theorem opair.eq [a b c d : term] :
103    |- ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d)
104proof
105    hence ⟨a, b⟩ = ⟨c, d⟩ → π₁(⟨a, b⟩) = π₁(⟨c, d⟩) by zfc.extensionality;
106    follows π₁(⟨a, b⟩) = π₁(⟨c, d⟩) ↔ a = c by opair_first.def;
107    follows ⟨a, b⟩ = ⟨c, d⟩ → π₂(⟨a, b⟩) = π₂(⟨c, d⟩) by zfc.extensionality;
108    follows π₂(⟨a, b⟩) = π₂(⟨c, d⟩) ↔ b = d by opair_second.def;
109    -- suffices ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d);
110    hence ⟨a, b⟩ = ⟨c, d⟩ → (a = c ∧ b = d) logically;
111    hence (a = c ∧ b = d) → ⟨a, b⟩ = ⟨c, d⟩ logically;
112    done logically
113qed

The Cartesian Product

The Cartesian product of two sets is the set of all ordered pairs formed from the elements of those sets. A double powerset is sufficient to make a superset of the Cartesian product from which we can then restrict to get the required set.

122notation product
123    term (350) ::= term " × " term
124end

126definition
127    A × B := {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
128end

The difficult task is to prove that this gives us every possible ordered pair.

132theorem cart_prod.def [A B : term] :
133    |- ∀x, x ∈ A × B ↔ ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩
134proof
135    arbitrary x;
136
137    -- remember the definition of A × B. (specifically have Vampire remember it)
138    follows A × B = {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
139        by eq.refl [A × B];
140
141    -- the forward direction is pretty simple. it just comes directly from the
142    -- definition of restricted comprehension.
143    assume x ∈ A × B then ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ logically;
144
145    -- the other direction is harder. it follows quickly that x satisfies the
146    -- comprehension condition, but it is a little more work to show it is in
147    -- the double powerset.
148    assume ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ then x ∈ A × B as
149        obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ logically;
150        follows x = {{a}, {a, b}} by_def x = ⟨a, b⟩;
151
152        -- we already have that x is a pair so we just need to prove it is in the powerset
153        suffices x ∈ 𝒫(𝒫(A ∪ B)) ∧ (∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩) logically;
154        suffices x ∈ 𝒫(𝒫(A ∪ B)) given x = ⟨a, b⟩;
155
156        follows a ∈ A ∪ B ∧ b ∈ A ∪ B    by union.def given a ∈ A and b ∈ B;
157        thus  {a}          ∈   𝒫(A ∪ B)  by powset.singleton_in;
158        thus       {a, b}  ∈   𝒫(A ∪ B)  by powset.pair_in;
159        thus {{a}, {a, b}} ∈ 𝒫(𝒫(A ∪ B)) by powset.pair_in;
160        thus             x ∈ 𝒫(𝒫(A ∪ B)) given x = {{a}, {a, b}};
161    ;
162
163    done logically
164qed

Next, we prove a useful result relating the cartesian product of sets to their subsets.

168lemma cart_prod.sub [A B C D : term] : (A ⊆ C) (B ⊆ D)
169    |- A × B ⊆ C × D
170proof
171    suffices ∀x ∈ A × B, x ∈ C × D;
172    arbitrary x;
173    assume x ∈ A × B then x ∈ C × D as
174        obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
175        follows a ∈ C by sub.def given A ⊆ C;
176        follows b ∈ D by sub.def given B ⊆ D;
177        done by cart_prod.def
178        ;
179    done logically
180qed

We can define the set of binary relations between two sets as the powerset of the Cartesian product of those two sets. Conceptually, if $R$ is a relation between $A$ and $B$ then it is the set of all pairs $(a, b)$ where $a$ and $b$ are related by $R$.

188notation term.with_term_term
189    term (1000) ::= @name "(" term ", " term ")"
190end

192definition
193    Rel(A, B) := 𝒫(A × B)
194end

196theorem rel_on.def [A B : term] :
197    |- ∀R, R ∈ Rel(A, B) ↔ R ⊆ A × B
198proof
199    follows Rel(A, B) = 𝒫(A × B) by eq.refl [Rel(A, B)];
200    done by powset.def
201qed

For a relation we have the notions of the domain and range which are the sets of the first element of each pair and the second element of each pair, respectively.

207definition
208    dom(R) := {π₁(x) | x ∈ R}
209end

211definition
212    ran(R) := {π₂(x) | x ∈ R}
213end

We can prove the following using the set map definition.

217theorem dom.def [R : term] :
218    |- ∀x, x ∈ dom(R) ↔ ∃y ∈ R, x = π₁(y)
219proof
220    suffices ∀x, x ∈ {π₁(z) | z ∈ R} ↔ ∃y ∈ R, x = π₁(y);
221    thus ∀x, x ∈ {π₁(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₁(z)) by set_map.def [π₁(_)] [R];
222    done logically
223qed

225theorem ran.def [R : term] :
226    |- ∀x, x ∈ ran(R) ↔ ∃y ∈ R, x = π₂(y)
227proof
228    suffices ∀x, x ∈ {π₂(z) | z ∈ R} ↔ ∃y ∈ R, x = π₂(y);
229    thus ∀x, x ∈ {π₂(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₂(z)) by set_map.def [π₂(_)] [R];
230    done logically
231qed

We can also have the notion of being a relation without having to know the exact domain and range.

236notation postfix_pred
237    sentence ::= term " : " @name
238end

240definition
241    R : Rel := R ∈ Rel(dom(R), ran(R))
242end

244theorem rel.def [R : term] :
245    |- R : Rel ↔ R ∈ Rel(dom(R), ran(R))
246proof
247    done by iff.refl [R : Rel]
248qed

The following result can be proved using the different relation definitions as well as the definition of the domain and range.

252theorem rel.is_rel_on [R : term] :
253    |- R : Rel ↔ ∃A, ∃B, R ∈ Rel(A, B)
254proof
255    -- (→)
256    assume R : Rel then ∃A, ∃B, R ∈ Rel(A, B) as
257        follows R ∈ Rel(dom(R), ran(R)) by rel.def;
258        done logically;
259    -- (←)
260    assume ∃A, ∃B, R ∈ Rel(A, B) then R : Rel as
261        -- We can fix A and B with our assumption
262        obtain A st ∃B, R ∈ Rel(A, B) logically;
263        obtain B st R ∈ Rel(A, B) logically;
264        follows R ⊆ A × B by rel_on.def;
265        suffices R ∈ Rel(dom(R), ran(R)) by rel.def;
266        suffices R ⊆ dom(R) × ran(R) by rel_on.def;
267        suffices ∀x, x ∈ R → x ∈ dom(R) × ran(R) by sub.def;
268        arbitrary x;
269        assume x ∈ R then x ∈ dom(R) × ran(R) as
270            follows ∀y, y ∈ R → y ∈ A × B by sub.def given R ⊆ A × B;
271            follows x ∈ A × B logically;
272            -- As x is an ordered pair in A × B, we know specifically that there is an a and b which make up the ordered pair x
273            obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
274            -- TODO: This (2 next lines) should not be something we have to prove
275            follows π₁(x) = a by opair_first.def given x = ⟨a, b⟩;
276            follows π₂(x) = b by opair_second.def given x = ⟨a, b⟩;
277            -- The first and second coordinates of x are by definition in the domain and range of R
278            thus π₁(x) ∈ dom(R) by dom.def given x ∈ R;
279            thus π₂(x) ∈ ran(R) by ran.def given x ∈ R;
280            done by cart_prod.def;
281        ;
282    done logically
283qed

We can show this fact in a similar manner to the previous proof, additionally making use of our cartesian product subset lemma.

286theorem rel_on.is_rel [R A B : term] :
287    |- R ∈ Rel(A, B) ↔ (R : Rel ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B)
288proof
289    -- If R is a relation, then its a relation between sets
290    follows R : Rel ↔ ∃C, ∃D, R ∈ Rel(C, D) by rel.is_rel_on;
291    suffices R ∈ Rel(A, B) ↔ ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) logically;
292    -- (→)
293    assume R ∈ Rel(A, B) then ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) as
294        -- Really we just have to show that dom(R) ⊆ A and ran(R) ⊆ B as the first proposition is the same as our assumption
295        hence R ⊆ A × B by rel_on.def;
296        hence ∃C, ∃D, R ⊆ C × D logically;
297        follows ∃C, ∃D, R ∈ Rel(C, D) by rel_on.def;
298        suffices dom(R) ⊆ A ∧ ran(R) ⊆ B logically;
299        suffices (∀x ∈ dom(R), x ∈ A) ∧ (∀y ∈ ran(R), y ∈ B) by sub.def;
300        suffices (∀x, x ∈ dom(R) → x ∈ A) ∧ (∀y, y ∈ ran(R) → y ∈ B) logically;
301        -- Similarly to the last proof, we want to show the statement holds for an arbitrary element
302        hence (∀x, x ∈ dom(R) → x ∈ A) as
303            arbitrary x;
304            assume x ∈ dom(R) then x ∈ A as
305                obtain z st z ∈ R ∧ x = π₁(z) by dom.def;
306                follows z ∈ A × B by sub.def given R ⊆ A × B;
307                obtain a st a ∈ A and b st b ∈ B ∧ z = ⟨a, b⟩ by cart_prod.def;
308                follows π₁(z) = a by opair_first.def given z = ⟨a, b⟩;
309                done logically
310                ;
311            done logically
312            ;
313        hence (∀y, y ∈ ran(R) → y ∈ B) as
314            arbitrary y;
315            assume y ∈ ran(R) then y ∈ B as
316                obtain z st z ∈ R ∧ y = π₂(z) by ran.def;
317                follows z ∈ A × B by sub.def given R ⊆ A × B;
318                obtain b st b ∈ B and a st a ∈ A ∧ z = ⟨a, b⟩ by cart_prod.def;
319                follows π₂(z) = b by opair_second.def given z = ⟨a, b⟩;
320                done logically
321                ;
322            done logically
323            ;
324        done logically
325    ;
326    -- (←)
327    assume ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) then R ∈ Rel(A, B) as
328        hence R : Rel by rel.is_rel_on;
329        follows R ∈ Rel(dom(R), ran(R)) by rel.def;
330        thus R ⊆ dom(R) × ran(R) by rel_on.def;
331        -- TODO: is this lemma useful?
332        follows dom(R) × ran(R) ⊆ A × B by cart_prod.sub;
333        hence R ⊆ A × B by sub.def given R ⊆ dom(R) × ran(R);
334        done by rel_on.def
335        ;
336    done logically
337qed

A functional relation is a particular kind of binary relation where the first element of each ordered pair in the relation is unique.

342notation functional_relation
343    term ::= term " → " term
344end

346definition
347    A → B := {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f}
348end

350theorem fn_on.def [A B : term] :
351    |- ∀f, f ∈ (A → B) ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f
352proof
353    suffices ∀f, f ∈ {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f;
354    done by zfc.extensionality
355qed

And once again we can define the notion of being a function independent of the domain and range.

360definition
361    f : Fn := f ∈ (dom(f) → ran(f))
362end

364theorem fn.def [f : term] :
365    |- f : Fn ↔ f ∈ (dom(f) → ran(f))
366proof
367    done by iff.refl [f : Fn]
368qed

370lemma fn.in_rel [A B : term] :
371    |- (A → B) ⊆ Rel(A, B)
372proof
373    thus {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ⊆ Rel(A, B)
374        by comp.sub [∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ _] [Rel(A, B)];
375qed

377theorem fn.is_fn_on [f : term] :
378    |- f : Fn ↔ ∃A, ∃B, f ∈ (A → B)
379proof
380    suffices f ∈ (dom(f) → ran(f)) ↔ ∃A, ∃B, f ∈ (A → B);
381    assume f ∈ (dom(f) → ran(f)) then ∃A, ∃B, f ∈ (A → B) logically;
382    assume ∃A, ∃B, f ∈ (A → B) then f ∈ (dom(f) → ran(f)) as
383        obtain A st ∃B, f ∈ (A → B) logically;
384        obtain B st f ∈ (A → B) logically;
385        hence f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
386        follows f : Rel by rel.is_rel_on;
387        follows f ∈ Rel(dom(f), ran(f)) by rel.def;
388        follows dom(f) ⊆ A by rel_on.is_rel;
389        follows ∀a, a ∈ dom(f) → a ∈ A by sub.def given dom(f) ⊆ A;
390        hence ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f logically;
391        done by fn_on.def
392        ;
393    done logically
394qed

396theorem fn_on.is_fn [f A B : term] :
397    |- f ∈ (A → B) ↔ (f : Fn ∧ dom(f) = A ∧ ran(f) ⊆ B)
398proof
399    hence f: Fn ↔ ∃C, ∃D, f ∈ (C → D) by fn.is_fn_on;
400    suffices f ∈ (A → B) ↔ (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) logically;
401    assume f ∈ (A → B) then (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) as
402        hence ∃C, ∃D, f ∈ (C → D) logically;
403        thus ∀x, x ∈ (A → B) → ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ x by fn_on.def;
404        follows ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
405        suffices dom(f) = A ∧ ran(f) ⊆ B logically;
406        follows (A → B) ⊆ Rel(A, B) by fn.in_rel;
407        follows f ∈ Rel(A, B) by sub.def given (A → B) ⊆ Rel(A, B);
408        follows dom(f) ⊆ A ∧ ran(f) ⊆ B by rel_on.is_rel;
409        suffices A ⊆ dom(f) by sub.sub_eq;
410        suffices ∀a ∈ A, a ∈ dom(f) by sub.def;
411        arbitrary a;
412        assume a ∈ A then a ∈ dom(f) as
413            obtain b st ⟨a, b⟩ ∈ f logically;
414            thus a = π₁(⟨a, b⟩) by opair_first.def;
415            done by dom.def given ⟨a, b⟩ ∈ f
416            ;
417        done logically
418        ;
419    assume (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) then f ∈ (A → B) as
420        obtain C st ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B logically;
421        obtain D st f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B logically;
422        follows f : Fn by fn.is_fn_on;
423        follows f ∈ (dom(f) → ran(f)) by fn.def;
424        follows ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
425        hence ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
426        follows (C → D) ⊆ Rel(C, D) by fn.in_rel;
427        follows f ∈ Rel(C, D) by sub.def given (C → D) ⊆ Rel(C, D);
428        follows f : Rel by rel.is_rel_on;
429        hence dom(f) = A logically;
430        follows dom(f) ⊆ dom(f) by sub.refl;
431        follows dom(f) ⊆ A by eq.subst [dom(f) ⊆ _] [dom(f)] [A];
432        follows f ∈ Rel(A, B) by rel_on.is_rel;
433        done by fn_on.def
434        ;
435    done logically
436qed

We define function application by extracting the second element of the unique ordered pair which has the argument as the first element. We can make this definition using the iota operator.

442notation function_application
443    term (1000) ::= term "(" term ")"
444end

446definition
447    f:term (a) := ℩b, ⟨a, b⟩ ∈ f
448end

This proof follows from our definition as well as the iota operator which lets us show unambiguity

452theorem fn_on.pairs [f A B : term] : (f ∈ (A → B))
453    |- f = {⟨a, f(a)⟩ | a ∈ A}
454proof
455    suffices f = {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩};
456    thus f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
457    follows f ⊆ A × B by rel_on.def;
458    follows ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
459    thus ∀x, x ∈ f ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) as
460        arbitrary x;
461        assume x ∈ f then ∃a, a ∈ A ∧ x = ⟨a, f(a)⟩ as
462            follows x ∈ A × B by sub.def given f ⊆ A × B;
463            obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
464            follows ⟨a, b⟩ ∈ f given x = ⟨a, b⟩;
465            follows ∃!b, ⟨a, b⟩ ∈ f logically;
466            follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
467            hence f(a) = b logically;
468            hence x = ⟨a, f(a)⟩ logically;
469            done logically
470            ;
471        assume ∃a, a ∈ A ∧ x = ⟨a, f(a)⟩ then x ∈ f as
472            obtain a st a ∈ A ∧ x = ⟨a, f(a)⟩ logically;
473            follows ∃!b, ⟨a, b⟩ ∈ f logically;
474            follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
475            done logically
476            ;
477        done logically
478        ;
479    -- f itself witnesses that the set exists, so the comprehension is well
480    -- defined and has the expected members.
481    follows ∃z, ∀x, x ∈ z ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) logically;
482    follows ∀x, x ∈ {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩} ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) by uncomp.def [∃a, a ∈ A ∧ _ = ⟨a, f(a)⟩];
483    follows ∀x, x ∈ f ↔ x ∈ {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩} logically;
484    done by zfc.extensionality
485qed

487theorem fn.pairs [f : term] : (f : Fn)
488    |- f = {⟨x, f(x)⟩ | x ∈ dom(f)}
489proof
490    follows f ∈ (dom(f) → ran(f)) by fn.def;
491    done by fn_on.pairs [f] [dom(f)] [ran(f)]
492qed

A useful lemma which lets us skip a lot of notation

496lemma fn.apply_iff [f a b : term] : (f : Fn) (a ∈ dom(f))
497    |- ⟨a, b⟩ ∈ f ↔ f(a) = b
498proof
499    follows f ∈ (dom(f) → ran(f)) by fn.def;
500    follows ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
501    follows ∃!b, ⟨a, b⟩ ∈ f logically;
502    follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
503    done logically
504qed

507notation function_maps_to
508    term ::= x:@binding(term) " ∈ " term " ↦ " term(x)
509end

511definition
512    x ∈ X ↦ f(x) := {⟨x, f(x)⟩ | x ∈ X}
513end

This theorem follows from an ever-rare explicit use of the axiom of replacement as well as previously shown results for relations.

517theorem fun_map.is.rel [A B : term] [f(_) : term(term)]: (∀x ∈ A, f(x) ∈ B)
518    |- x ∈ A ↦ f(x) ∈ (A → B)
519proof
520    suffices {⟨x, f(x)⟩ | x ∈ A} ∈ (A → B);
521    suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ (A → B);
522    -- Using our replacement axiom to show that a functional mapping of a set defines its own set
523    follows ∀a, (∀x, x ∈ a → ∃!y, y = ⟨x, f(x)⟩) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ y = ⟨z, f(z)⟩))
524        by zfc.replacement [_1 = ⟨_0, f(_0)⟩];
525    -- Then we show the set that it defines
526    follows ∃z, ∀y, y ∈ z ↔ (∃x, x ∈ A ∧ y = ⟨x, f(x)⟩) logically;
527    thus ∀y, y ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ↔ (∃x, x ∈ A ∧ y = ⟨x, f(x)⟩)
528        by uncomp.def [∃x, x ∈ A ∧ _ = ⟨x, f(x)⟩];
529    suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ Rel(A, B)
530        ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} by fn_on.def;
531    -- Function mappings are subsets of all of the relations between two sets
532    thus {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ Rel(A, B) as
533        suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ⊆ A × B by rel_on.def;
534        suffices ∀w, w ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} → w ∈ A × B by sub.def;
535        arbitrary w;
536        assume w ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} then w ∈ A × B as
537            obtain a st a ∈ A ∧ w = ⟨a, f(a)⟩ logically;
538            follows f(a) ∈ B logically;
539            done by cart_prod.def
540            ;
541        done logically
542        ;
543    -- Showing function well-definedness, basically that every element a in A has a mapping, and that a = a → f(a) = f(a)
544    thus ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} as
545        arbitrary a;
546        assume a ∈ A then ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} as
547            thus ⟨a, f(a)⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} logically;
548            thus ∀b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} → b = f(a) as
549                arbitrary b;
550                assume ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} then b = f(a) as
551                    obtain c st c ∈ A ∧ ⟨a, b⟩ = ⟨c, f(c)⟩ logically;
552                    follows a = c ∧ b = f(c) by opair.eq;
553                    done logically
554                    ;
555                done logically
556                ;
557            done logically
558            ;
559        done logically
560        ;
561
562    done logically
563qed

TODO:

568grammar_category chain_list

570tactic tactic.chain
571    tactic ::= @kw"chain" term:@fragment(term) list:chain_list
572end

574tactic chain_list.one
575    chain_list ::= "=" term:@fragment(term) just:justification ";"
576end

577tactic chain_list.many
578    chain_list ::= "=" term:@fragment(term) just:justification ";" rest:chain_list
579end

582theorem fn.eq_on_dom.eq [f g : term] : (f : Fn) (g : Fn) (dom(f) = dom(g))
583    (∀x ∈ dom(f), f(x) = g(x))
584    |- f = g
585proof
586    -- chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} by fn.pairs;
587    --         = {⟨x, g(x)⟩ | x ∈ dom(f)} given ∀x ∈ dom(f), f(x) = g(x);
588    --         = {⟨x, g(x)⟩ | x ∈ dom(g)} given dom(f) = dom(g);
589    --         = g                        by fn.pairs;
590    chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} as todo;
591            = {⟨x, g(x)⟩ | x ∈ dom(f)} as todo;
592            = {⟨x, g(x)⟩ | x ∈ dom(g)} as todo;
593            = g                        as todo;
594qed

596notation fn_restriction
597    term ::= term " ↾ " term
598end

600definition
601    f ↾ A := {x ∈ f | π₁(x) ∈ A}
602end

604theorem fn.restriction.is [f X : term] : (f : Fn)
605    |- f ↾ X : Fn
606proof
607    todo
608qed

610theorem fn.restriction.pairs [f X : term] : (f : Fn)
611    |- f ↾ X = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X}
612proof
613    todo
614qed

616theorem fn.restriction.eq [f g X : term] : (f : Fn) (g : Fn) (dom(f) ∩ X = dom(g) ∩ X)
617    (∀x ∈ dom(f) ∩ X, f(x) = g(x))
618    |- f ↾ X = g ↾ X
619proof
620    -- chain f ↾ X 
621    --     = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} by fn.restriction.pairs;
622    --     = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} given ∀x ∈ X, f(x) = g(x);
623    --     = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} given dom(f) ∩ X = dom(g) ∩ X;
624    --     = g ↾ X                        by fn.restriction.pairs;
625    chain f ↾ X 
626        = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} as todo;
627        = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} as todo;
628        = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} as todo;
629        = g ↾ X                        as todo;
630qed

Function properties & Composition 3.4

The image of a function under a set is the set resulting from applying the function to every element of the set

636notation image_set
637    term (1000) ::= term "[" term "]"
638end

640definition
641    f:term [A] := {f(a) | a ∈ A}
642end

644theorem image.def [f A : term] :
645    |- ∀y, y ∈ f[A] ↔ ∃a ∈ A, y = f(a)
646proof
647    suffices ∀y, y ∈ {f(a) | a ∈ A} ↔ ∃a ∈ A, y = f(a);
648    thus ∀y, y ∈ {f(a) | a ∈ A} ↔ (∃a, a ∈ A ∧ y = f(a)) by set_map.def [f(_)] [A];
649    done logically
650qed

Trivially, the image of a subset of a domain is a subset of the range, with equality when finding the image of the domain

654theorem dom.is_ran_under_image [f A B : term] : (f ∈ (A → B))
655    |- f[A] = ran(f)
656proof
657    thus f : Fn by fn_on.is_fn;
658    suffices f[dom(f)] = ran(f) by fn_on.is_fn;
659    hence ∀y, y ∈ f[dom(f)] ↔ ∃a ∈ dom(f), y = f(a) by image.def;
660    furthermore ∀y, y ∈ ran(f) ↔ ∃z ∈ f, y = π₂(z) by ran.def;
661    indeed ∀y, y ∈ f[dom(f)] ↔ y ∈ ran(f) as
662        arbitrary y;
663        assume y ∈ f[dom(f)] then y ∈ ran(f) as
664            obtain a st a ∈ dom(f) ∧ y = f(a) logically;
665            hence ⟨a, f(a)⟩ ∈ f ↔ f(a) = f(a) by fn.apply_iff given a ∈ dom(f);
666            follows π₂(⟨a, f(a)⟩) = f(a) by opair_second.def;
667            done by ran.def given ⟨a, f(a)⟩ ∈ f
668            ;
669        assume y ∈ ran(f) then y ∈ f[dom(f)] as
670            follows f ⊆ A × B by rel_on.def, fn.in_rel, sub.def;
671            obtain b st b ∈ f ∧ y = π₂(b) logically;
672            hence b ∈ A × B by sub.def;
673            obtain a st a ∈ A and c st c ∈ B ∧ b = ⟨a, c⟩ by cart_prod.def;
674            furthermore π₂(b) = c by opair_second.def given b = ⟨a, c⟩;
675            thus a = π₁(⟨a, c⟩) by opair_first.def;
676            thus ⟨a, c⟩ ∈ f given b = ⟨a, c⟩;
677            hence a ∈ dom(f) by dom.def given ⟨a, c⟩ ∈ f;
678            follows ⟨a, c⟩ ∈ f ↔ f(a) = c by fn.apply_iff [f] [a] [c];
679            follows f(a) = y logically;
680            done by image.def given a ∈ dom(f)
681            ;
682        done logically
683        ;
684    done by zfc.extensionality
685qed

Importantly, every image has a preimage, which we'll have as the set of terms which are mapped to a specific set under a function

690notation preimage_set
691    term (1000) ::= term "⁻¹" "[" term "]"
692end

694definition
695    f:term⁻¹[A] := {x ∈ dom(f) | f(x) ∈ A}
696end

698theorem preimage.def [f A : term] :
699    |- ∀x, x ∈ f⁻¹[A] ↔ (x ∈ dom(f) ∧ f(x) ∈ A)
700proof
701    suffices ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ A} ↔ (x ∈ dom(f) ∧ f(x) ∈ A);
702    done by zfc.extensionality
703qed

A surjection, also known as an onto function, between sets is a mapping where the range is the same as the codomain

707notation surjection
708    term ::= term " ↠ " term
709end

711definition
712    A ↠ B := {f ∈ (A → B) | ran(f) = B}
713end

715theorem surj_on.def [A B : term] :
716    |- ∀f, f ∈ (A ↠ B) ↔ (f ∈ (A → B) ∧ ran(f) = B)
717proof
718    suffices ∀f, f ∈ {f ∈ (A → B) | ran(f) = B} ↔ (f ∈ (A → B) ∧ ran(f) = B);
719    done by zfc.extensionality
720qed

An injection, a one-to-one function, between sets is one where every element of the domain is mapped to a unique element in the range

724notation injection
725    term ::= term " ↣ " term
726end

728definition
729    A ↣ B := {f ∈ (A → B) | ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y}
730end

732theorem inj_on.def [A B : term] :
733    |- ∀f, f ∈ (A ↣ B) ↔ (f ∈ (A → B) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y))
734proof
735    suffices ∀f, f ∈ {f ∈ (A → B) | ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y} ↔ (f ∈ (A → B) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y));
736    done by zfc.extensionality
737qed

739definition
740    f : Inj := f ∈ (dom(f) ↣ ran(f))
741end

743theorem inj.def [f : term] :
744    |- f : Inj ↔ f ∈ (dom(f) ↣ ran(f))
745proof
746    done by iff.refl [f : Inj]
747qed

A bijection between sets is a function that is both injective and surjective

751notation bijection
752    term ::= term " ↔ " term
753end

755definition
756    A ↔ B := {f ∈ (A ↣ B) | ran(f) = B}
757end

759theorem bij_on.def [A B : term] :
760    |- ∀f, f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ ran(f) = B)
761proof
762    suffices ∀f, f ∈ {f ∈ (A ↣ B) | ran(f) = B} ↔ (f ∈ (A ↣ B) ∧ ran(f) = B);
763    done by zfc.extensionality
764qed

766definition
767    f : Bij := f ∈ (dom(f) ↔ ran(f))
768end

770theorem bij.def [f : term] :
771    |- f : Bij ↔ f ∈ (dom(f) ↔ ran(f))
772proof
773    done by iff.refl [f : Bij]
774qed

This theorem follows cleanly from the definitions for injective, bijective, and surjective functions

778theorem bij_on.is_inj_and_surj [f A B : term] :
779    |- f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ f ∈ (A ↠ B))
780proof
781    follows f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ ran(f) = B) by bij_on.def;
782    follows f ∈ (A ↠ B) ↔ (f ∈ (A → B) ∧ ran(f) = B) by surj_on.def;
783    follows f ∈ (A ↣ B) → f ∈ (A → B) by inj_on.def;
784    done logically
785qed

We can define an inverse relation simply as the swapped coordinates of the relation

789notation inverse_relation
790    term (1000) ::= term "⁻¹"
791end

793definition
794    f:term⁻¹ := {⟨π₂(p), π₁(p)⟩ | p ∈ f}
795end

Swapping the components of every pair in f swaps the roles of the domain and the range.

799lemma inv.dom [f : term] :
800    |- dom(f⁻¹) = ran(f)
801proof
802    follows ∀x, x ∈ dom(f⁻¹) ↔ ∃y ∈ f⁻¹, x = π₁(y) by dom.def;
803    thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
804    follows ∀p, π₁(⟨π₂(p), π₁(p)⟩) = π₂(p) by opair_first.def;
805    follows ∀x, x ∈ ran(f) ↔ ∃p ∈ f, x = π₂(p) by ran.def;
806    hence ∀x, x ∈ dom(f⁻¹) ↔ x ∈ ran(f) logically;
807    done by zfc.extensionality
808qed

810lemma inv.ran [f : term] :
811    |- ran(f⁻¹) = dom(f)
812proof
813    follows ∀x, x ∈ ran(f⁻¹) ↔ ∃y ∈ f⁻¹, x = π₂(y) by ran.def;
814    thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
815    follows ∀p, π₂(⟨π₂(p), π₁(p)⟩) = π₁(p) by opair_second.def;
816    follows ∀x, x ∈ dom(f) ↔ ∃p ∈ f, x = π₁(p) by dom.def;
817    hence ∀x, x ∈ ran(f⁻¹) ↔ x ∈ dom(f) logically;
818    done by zfc.extensionality
819qed

The following proof gives us a way to reason with and construct what f⁻¹ looks like

823lemma inv.mem [f A B : term] : (f ∈ Rel(A, B))
824    |- ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f
825proof
826    arbitrary a; arbitrary b;
827    follows f ⊆ A × B by rel_on.def;
828    thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
829    assume ⟨b, a⟩ ∈ f then ⟨a, b⟩ ∈ f⁻¹ as
830        follows π₁(⟨b, a⟩) = b by opair_first.def;
831        follows π₂(⟨b, a⟩) = a by opair_second.def;
832        hence ⟨a, b⟩ = ⟨π₂(⟨b, a⟩), π₁(⟨b, a⟩)⟩ logically;
833        done logically
834        ;
835    assume ⟨a, b⟩ ∈ f⁻¹ then ⟨b, a⟩ ∈ f as
836        obtain p st p ∈ f ∧ ⟨a, b⟩ = ⟨π₂(p), π₁(p)⟩ logically;
837        follows p ∈ A × B by sub.def given f ⊆ A × B;
838        obtain c st c ∈ A and d st d ∈ B ∧ p = ⟨c, d⟩ by cart_prod.def;
839        follows π₁(p) = c by opair_first.def given p = ⟨c, d⟩;
840        follows π₂(p) = d by opair_second.def given p = ⟨c, d⟩;
841        follows a = d ∧ b = c by opair.eq given ⟨a, b⟩ = ⟨π₂(p), π₁(p)⟩;
842        done logically
843        ;
844    done logically
845qed

The inverse of a relation between A and B is itself a relation, between B and A.

849lemma inv.rel [f A B : term] : (f ∈ Rel(A, B))
850    |- f⁻¹ ∈ Rel(B, A)
851proof
852    -- A relation is just some subset of the cartesian product
853    follows f ⊆ A × B by rel_on.def;
854    follows ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f by inv.mem;
855    suffices ∀y, y ∈ f⁻¹ → y ∈ B × A by rel_on.def, sub.def;
856    arbitrary y;
857    assume y ∈ f⁻¹ then y ∈ B × A as
858        -- every element of f⁻¹ is a swapped pair from f
859        thus ∀z, z ∈ f⁻¹ ↔ ∃p ∈ f, z = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
860        obtain p st p ∈ f ∧ y = ⟨π₂(p), π₁(p)⟩ logically;
861        -- inv.mem swaps the pair back into f
862        follows ⟨π₁(p), π₂(p)⟩ ∈ f by inv.mem;
863        follows ⟨π₁(p), π₂(p)⟩ ∈ A × B by sub.def given f ⊆ A × B;
864        hence π₁(p) ∈ A ∧ π₂(p) ∈ B by cart_prod.def, opair.eq;
865        done by cart_prod.def
866        ;
867qed

When f is a bijection, its inverse is a function, every b ∈ B has a preimage because f is onto, and that preimage is unique because f is injective.

872lemma inv.is_fn_on [f A B : term] : (f ∈ (A ↔ B))
873    |- f⁻¹ ∈ (B → A)
874proof
875    indeed f ∈ (A ↣ B) ∧ ran(f) = B by bij_on.def;
876    hence f ∈ (A → B) ∧ f : Fn ∧ dom(f) = A by inj_on.def, fn_on.is_fn;
877    furthermore ∀a, ∀b, a ∈ A ∧ b ∈ A ∧ f(a) = f(b) → a = b by inj_on.def;
878    furthermore f ∈ Rel(A, B) by fn.in_rel, sub.def;
879    follows f⁻¹ ∈ Rel(B, A) by inv.rel given f ∈ Rel(A, B);
880    thus ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f by inv.mem given f ∈ Rel(A, B);
881    suffices ∀b ∈ B, ∃!a, ⟨b, a⟩ ∈ f⁻¹ by fn_on.def;
882    arbitrary d;
883    assume d ∈ B then ∃!a, ⟨d, a⟩ ∈ f⁻¹ as
884        -- Every element of B is in the image of f[A] so a exists
885        obtain a₀ st a₀ ∈ A ∧ d = f(a₀) by image.def, dom.is_ran_under_image;
886        hence ⟨a₀, d⟩ ∈ f ∧ ⟨d, a₀⟩ ∈ f⁻¹ by fn.apply_iff given a₀ ∈ A;
887        -- any preimage of d is exactly a because f is injective
888        hence ∀a, ⟨d, a⟩ ∈ f⁻¹ → a ∈ dom(f) ∧ f(a) = d by dom.def, opair_first.def, fn.apply_iff;
889        done logically
890        ;
891    done logically
892qed

Next we show that bijections undo their inverse

896lemma inv.apply [f A B b : term] : (f ∈ (A ↔ B)) (b ∈ B)
897    |- f(f⁻¹(b)) = b
898proof
899    indeed f ∈ (A → B) ∧ f : Fn ∧ dom(f) = A by bij_on.def, inj_on.def, fn_on.is_fn;
900    furthermore f ∈ Rel(A, B) by fn.in_rel, sub.def;
901    hence ∀u, ∀v, ⟨u, v⟩ ∈ f⁻¹ ↔ ⟨v, u⟩ ∈ f by inv.mem;
902    follows f⁻¹ : Fn ∧ dom(f⁻¹) = B by inv.is_fn_on, fn_on.is_fn;
903    hence ⟨b, f⁻¹(b)⟩ ∈ f⁻¹ ∧ ⟨f⁻¹(b), b⟩ ∈ f by fn.apply_iff given b ∈ B;
904    follows f⁻¹(b) ∈ dom(f) by dom.def, opair_first.def given ⟨f⁻¹(b), b⟩ ∈ f;
905    done by fn.apply_iff given ⟨f⁻¹(b), b⟩ ∈ f and f⁻¹(b) ∈ dom(f)
906qed

908notation function_composition
909    term (400) ::= term " ∘ " term
910end

912definition
913    g ∘ f := {⟨x, g(f(x))⟩ | x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}}
914end

916theorem composition.def [f g : term] :
917    |- ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩
918proof
919    follows ∀y, y ∈ (g ∘ f) ↔ ∃x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}, y = ⟨x, g(f(x))⟩
920        by set_map.def [⟨_, g(f(_))⟩] [{x ∈ dom(f) | f(x) ∈ dom(g)}];
921    hence ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)} ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
922        by comp.def [f(_) ∈ dom(g)] [dom(f)];
923    done logically
924qed

926theorem composition.dom [f g : term] :
927    |- ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
928proof
929    follows ∀z, z ∈ dom(g ∘ f) ↔ ∃y ∈ (g ∘ f), z = π₁(y) by dom.def;
930    furthermore ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩ by composition.def;
931    indeed ∀x, π₁(⟨x, g(f(x))⟩) = x by opair_first.def;
932    done logically
933qed

Here we show that function composition is itself a function

937theorem composition.is_fn [f g : term] : (f : Fn) (g : Fn)
938    |- g ∘ f : Fn
939proof
940    -- We want to show that the composition is some functional relation between two sets
941    suffices ∃A, ∃B, g ∘ f ∈ (A → B) by fn.is_fn_on;
942    thus ∀x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}, g(f(x)) ∈ ran(g) as
943        -- The construction here is simple as we only pick x where f(x) is in dom(g), because
944        -- g(dom(g)) being in ran(g) falls out of the definition
945        arbitrary c st c ∈ {x ∈ dom(f) | f(x) ∈ dom(g)};
946        follows g(f(c)) ∈ ran(g) as
947            follows ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)} ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
948                by comp.def [f(_) ∈ dom(g)] [dom(f)];
949            thus f(c) ∈ dom(g) logically;
950            hence ⟨f(c), g(f(c))⟩ ∈ g ↔ g(f(c)) = g(f(c)) by fn.apply_iff [g] [f(c)] [g(f(c))];
951            hence ⟨f(c), g(f(c))⟩ ∈ g logically;
952            follows π₂(⟨f(c), g(f(c))⟩) = g(f(c)) by opair_second.def;
953            done by ran.def given ⟨f(c), g(f(c))⟩ ∈ g
954            ;
955        done logically
956        ;
957    -- g ∘ f is a functional mapping from dom(g ∘ f) to ran(g)
958    follows g ∘ f ∈ ({x ∈ dom(f) | f(x) ∈ dom(g)} → ran(g))
959        by fun_map.is.rel [{x ∈ dom(f) | f(x) ∈ dom(g)}] [ran(g)] [g(f(_))];
960    done logically
961qed

This theorem follows cleanly from the above facts.

965theorem composition.apply [f g a : term] : (f : Fn) (g : Fn) (a ∈ dom(g ∘ f))
966    |- (g ∘ f)(a) = g(f(a))
967proof
968    hence a ∈ dom(f) ∧ f(a) ∈ dom(g) by composition.dom;
969    furthermore ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩ by composition.def;
970    furthermore ⟨a, g(f(a))⟩ ∈ (g ∘ f) logically;
971    indeed g ∘ f : Fn by composition.is_fn;
972    furthermore ⟨a, g(f(a))⟩ ∈ (g ∘ f) ↔ (g ∘ f)(a) = g(f(a)) by fn.apply_iff [g ∘ f] [a] [g(f(a))];
973    done logically
974qed

976theorem composition.is_fn_on [f g A B C : term] : (f ∈ (A → B)) (g ∈ (B → C))
977    |- g ∘ f ∈ (A → C)
978proof
979    hence g ∘ f : Fn by composition.is_fn, fn.is_fn_on;
980    hence ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g)) by composition.dom;
981    follows f ∈ (A → B) → dom(f) = A ∧ ran(f) ⊆ B by fn_on.is_fn;
982    follows g ∈ (B → C) → dom(g) = B ∧ ran(g) ⊆ C by fn_on.is_fn;
983    indeed ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ A ∧ f(x) ∈ B) logically;
984    hence ∀x, x ∈ A → f(x) ∈ B as
985        arbitrary c st c ∈ A;
986        follows f(c) ∈ B as
987            indeed c ∈ dom(f) logically;
988            hence ⟨c, f(c)⟩ ∈ f as
989                indeed f : Fn by fn.is_fn_on;
990                thus ⟨c, f(c)⟩ ∈ f ↔ f(c) = f(c) by fn.apply_iff [f] [c] [f(c)];
991                done logically
992                ;
993            follows f(c) ∈ ran(f) by opair_second.def, ran.def given ⟨c, f(c)⟩ ∈ f;
994            done by sub.def given ran(f) ⊆ B
995            ;
996        ;
997    hence ∀x, x ∈ dom(g ∘ f) ↔ x ∈ A logically;
998    hence dom(g ∘ f) = A by zfc.extensionality;
999    thus ran(g ∘ f) ⊆ C as
1000        suffices ∀y, y ∈ ran(g ∘ f) → y ∈ C by sub.def;
1001        arbitrary y;
1002        assume y ∈ ran(g ∘ f) then y ∈ C as
1003            obtain p st p ∈ (g ∘ f) ∧ y = π₂(p) by ran.def;
1004            obtain x st (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ p = ⟨x, g(f(x))⟩ by composition.def;
1005            indeed g : Fn by fn.is_fn_on;
1006            furthermore f(x) ∈ dom(g) logically;
1007            follows ⟨f(x), g(f(x))⟩ ∈ g ↔ g(f(x)) = g(f(x)) by fn.apply_iff [g] [f(x)] [g(f(x))];
1008            hence ⟨f(x), g(f(x))⟩ ∈ g logically;
1009            follows g(f(x)) ∈ ran(g) by ran.def, opair_second.def given ⟨f(x), g(f(x))⟩ ∈ g;
1010            done by opair_second.def, sub.def given ran(g) ⊆ C
1011            ;
1012        done logically
1013        ;
1014    done by fn_on.is_fn
1015qed

A function composed of two injective functions is itself injective. This is a standard injectivity proof where we reason that g(f(x)) = g(f(y)) implies f(x) = f(y) which impliex x = y

1020theorem comp_inj.is_inj [f g A B C : term] : (f ∈ (A ↣ B)) (g ∈ (B ↣ C))
1021    |- g ∘ f ∈ (A ↣ C)
1022proof
1023    follows g ∘ f ∈ (A → C) by composition.is_fn_on, inj_on.def;
1024    suffices ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ (g ∘ f)(x) = (g ∘ f)(y) → x = y by inj_on.def;
1025    arbitrary x; arbitrary y;
1026    assume x ∈ A ∧ y ∈ A ∧ (g ∘ f)(x) = (g ∘ f)(y) then x = y as
1027        follows f ∈ (A → B) ∧ g ∈ (B → C) by inj_on.def;
1028        indeed (∀a, ∀b, a ∈ A ∧ b ∈ A ∧ f(a) = f(b) → a = b)
1029              ∧ (∀a, ∀b, a ∈ B ∧ b ∈ B ∧ g(a) = g(b) → a = b) by inj_on.def;
1030        indeed f : Fn ∧ g : Fn by fn.is_fn_on;
1031        thus dom(g ∘ f) = A ∧ dom(g) = B by fn_on.is_fn;
1032        hence x ∈ dom(g ∘ f) ∧ y ∈ dom(g ∘ f) logically;
1033        follows g(f(x)) = g(f(y)) by composition.apply;
1034        furthermore f(x) ∈ B ∧ f(y) ∈ B by composition.dom;
1035        thus f(x) = f(y) logically;
1036        done logically
1037        ;
1038    done logically
1039qed

The following proof where we show composition of surjective functions is surjective takes a different shape. We want to show that some c in ran(g) has a preimage in dom(g) and then that dom(g) = ran(f).

1044theorem comp_surj.is_surj [f g A B C : term] : (f ∈ (A ↠ B)) (g ∈ (B ↠ C))
1045    |- g ∘ f ∈ (A ↠ C)
1046proof
1047    follows g ∘ f ∈ (A → C) by composition.is_fn_on, surj_on.def;
1048    suffices ran(g ∘ f) = C by surj_on.def;
1049    follows f ∈ (A → B) ∧ ran(f) = B ∧ g ∈ (B → C) ∧ ran(g) = C by surj_on.def;
1050    hence f : Fn ∧ g : Fn by fn_on.is_fn;
1051    thus dom(f) = A ∧ dom(g) = B ∧ ran(g ∘ f) ⊆ C by fn_on.is_fn;
1052    thus f[A] = ran(f) ∧ g[B] = ran(g) ∧ (g ∘ f)[A] = ran(g ∘ f) by dom.is_ran_under_image;
1053    furthermore ∀y, y ∈ f[A] ↔ ∃z ∈ A, y = f(z) by image.def;
1054    follows ∀y, y ∈ g[B] ↔ ∃z ∈ B, y = g(z) by image.def;
1055    suffices C ⊆ ran(g ∘ f) by sub.sub_eq;
1056    suffices ∀c, c ∈ C → c ∈ ran(g ∘ f) by sub.def;
1057    arbitrary c;
1058    assume c ∈ C then c ∈ ran(g ∘ f) as
1059        obtain b st b ∈ B ∧ c = g(b) logically;
1060        obtain a st a ∈ A ∧ b = f(a) logically;
1061        thus a ∈ dom(g ∘ f) by composition.dom;
1062        follows (g ∘ f)(a) = c by composition.apply;
1063        done by image.def given a ∈ A
1064        ;
1065    done logically
1066qed

This lemma looks a bit weird, but the idea is that we want to be able to reason about where in B f has an inverse

1070lemma inj.is_bij_to_ran [f A B : term] : (f ∈ (A ↣ B))
1071    |- f ∈ (A ↔ ran(f))
1072proof
1073    suffices f ∈ (A ↣ ran(f)) by bij_on.def;
1074    suffices (f ∈ (A → ran(f))) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y) by inj_on.def;
1075    hence f : Fn ∧ dom(f) = A by fn_on.is_fn, inj_on.def;
1076    follows ran(f) ⊆ ran(f) by sub.refl;
1077    indeed f ∈ (A → ran(f)) by fn_on.is_fn;
1078    done by inj_on.def
1079qed

1081lemma sub.has_surj [S B : term]: (S ⊆ B) (S ≠ ∅)
1082    |- ∃h, h ∈ (B ↠ S)
1083proof
1084    todo
1085qed

One of the most important properties of a bijective function is that it defines a unique bijective inverse. The proof follows cleanly from the previous inverse theorems.

1090theorem bij.has_inverse [f A B : term] : (f ∈ (A ↔ B))
1091    |- f⁻¹ ∈ (B ↔ A)
1092proof
1093    follows f⁻¹ ∈ (B → A) by inv.is_fn_on;
1094    follows dom(f) = A by bij_on.def, inj_on.def, fn_on.is_fn;
1095    follows ran(f⁻¹) = A by inv.ran given dom(f) = A;
1096    thus ∀x, ∀y, x ∈ B ∧ y ∈ B ∧ f⁻¹(x) = f⁻¹(y) → x = y as
1097        arbitrary x; arbitrary y;
1098        assume x ∈ B ∧ y ∈ B ∧ f⁻¹(x) = f⁻¹(y) then x = y as
1099            follows f(f⁻¹(x)) = x ∧ f(f⁻¹(y)) = y by inv.apply;
1100            done logically
1101            ;
1102        done logically
1103        ;
1104    follows f⁻¹ ∈ (B ↣ A) by inj_on.def;
1105    done by bij_on.def
1106qed

Here we have that an injection between sets implies the existence of a surjection the other way. We'll use this lemma later to explicitly construct this surjection. This lemma follows from the previous few where we show a surjection from B to ran(f) via sub.has_surj and ran(f) to A via bij.has_inverse as inj.is_bij_to_ran gives us a bijection between A and ran(f)

1112lemma inj.is_inv_srj [f g A B : term] : (f ∈ (A ↣ B)) (A ≠ ∅)
1113    |- ∃g, g ∈ (B ↠ A)
1114proof
1115    follows f ∈ (A → B) by inj_on.def;
1116    hence f[A] = ran(f) by dom.is_ran_under_image;
1117    suffices ∃h, ∃w, h ∈ (B ↠ ran(f)) ∧ w ∈ (ran(f) ↠ A) by comp_surj.is_surj;
1118    hence ∃w, w ∈ (ran(f) ↠ A) as
1119        follows f ∈ (A ↔ ran(f)) by inj.is_bij_to_ran;
1120        furthermore ∃w₀, w₀ ∈ (ran(f) ↔ A) by bij.has_inverse;
1121        done by bij_on.is_inj_and_surj
1122        ;
1123    furthermore ran(f) ⊆ B by fn_on.is_fn;
1124    follows ran(f) ≠ ∅ by image.def, nonempty.has_element;
1125    hence ∃h, h ∈ (B ↠ ran(f)) by sub.has_surj;
1126    done by comp_surj.is_surj
1127qed

1129theorem shroeder_bernstein [A B : term] : (∃f, f ∈ (A ↣ B)) (∃g, g ∈ (B ↣ A))
1130    |- ∃h, h ∈ (A ↔ B)
1131proof
1132    todo
1133qed

The Ordinals 3.5

36module set.ordinal

Definitions

2module set.ordinal.def

Our first goal upon the completion of our development of set theory will be to define the natural numbers. We will not develop the natural numbers directly but we will instead consider them to be certain "ordinal" numbers. So we will start by developing the ordinals.

The intuitive definition of the ordinal numbers is as follows: The empty set is an ordinal number and any set which contains every previously defined ordinal is an ordinal number. The goal is to produce a canonical set with each "number" of elements. The problem is that this definition is recursive and we will need ordinals before we can define recursion. Luckily, the ordinals admit an alternate definition. We define an ordinal as a transitive set that is well ordered by $\in$.

A transitive set is one where every element is also a subset.

16definition 
17    transitive(α) := ∀x ∈ α, x ⊆ α
18end

20theorem transitive.def [α : term] :
21    |- transitive(α) ↔ ∀x ∈ α, x ⊆ α
22proof
23    done by iff.refl [transitive(α)]
24qed

A well ordered set is one where every non-empty subset has a least element.

28definition
29    is_least(α, β) := α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ)
30end

32theorem is_least.def [α β : term] :
33    |- is_least(α, β) ↔ α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ)
34proof
35    done by iff.refl [is_least(α, β)]
36qed

38definition
39    well_ordered(α) := ∀β, β ⊆ α ∧ β ≠ ∅ → ∃γ, is_least(γ, β)
40end

42theorem well_ordered.def [α : term] :
43    |- well_ordered(α) ↔ ∀β, β ⊆ α ∧ β ≠ ∅ → ∃γ, is_least(γ, β)
44proof
45    done by iff.refl [well_ordered(α)]
46qed

The combination of these two properties is what defines an ordinal.

50definition
51    α : Ord := transitive(α) ∧ well_ordered(α)
52end

54theorem ordinal.def [α : term] :
55    |- α : Ord ↔ transitive(α) ∧ well_ordered(α)
56proof
57    done by iff.refl [α : Ord]
58qed

Since $\in$ well orders an ordinal, we can think of $\in$ as being $<$ for ordinals. It would be helpful, then, to know that $\in$ is anti-reflexive and anti-symmetric. These two properties follows by classic proofs from the axiom of regularity.

65lemma mem.irrefl [a : term] : 
66    |- a ∉ a
67proof
68    follows ∃x, x ∈ {a} by singleton.def;
69    obtain y st y ∈ {a} ∧ ¬∃z, (z ∈ y ∧ z ∈ {a}) by zfc.regularity;
70    done by singleton.def
71qed

73lemma mem.no_loop [a b : term] :
74    |- ¬(a ∈ b ∧ b ∈ a)
75proof
76    follows ∃x, x ∈ {a, b} by pair.def;
77    obtain y st y ∈ {a, b} ∧ ¬∃z, (z ∈ y ∧ z ∈ {a, b}) by zfc.regularity;
78    -- if y = a then b ∈ a ∧ b ∈ {a, b} would lead to a contradiction and 
79    -- vice versa. just let vampire work it out.
80    done by pair.def
81qed

Our First Ordinals

5module set.ordinal.basic

We are now ready for our first proof about ordinals. Recall from our intuative definition that we wanted $\empty$ to be the first ordinal number. Another way of thinking about this is that $\alpha < \beta$ can be thought of as $\alpha \in \beta$ and any ordinal is the set of every previous ordinal. Thus, it stands to reason that the first ordinal is $\empty$. The proof that $\empty$ satisfies our definition is easy; the two required properties are vacuous when applied to the empty set.

9theorem ordinal.empty.is :
10    |- ∅ : Ord
11proof
12    follows transitive(∅) as
13        suffices ∀x ∈ ∅, x ⊆ ∅ by transitive.def;
14        follows ∀x, x ∉ ∅ by empty.def;
15        done logically
16    ;
17
18    follows well_ordered(∅) as
19        suffices ∀β, β ⊆ ∅ ∧ β ≠ ∅ → ∃γ, is_least(γ, β) by well_ordered.def;
20        follows  ∀β, β ⊆ ∅ → β = ∅ by empty.sub_is_empty;
21        done logically
22    ;
23
24    thus ∅ : Ord by ordinal.def given transitive(∅) and well_ordered(∅);
25qed

The empty set is the zero of the ordinal numbers. We can get the next ordinal from any previous ordinal number by applying the successor operation. If $n$ is an ordinal then it is the set of all previous ordinals. So the next ordinal after $n$ should include all the ordinals in $n$ and $n$ itself. Hence the definition.

33definition
34    succ(n) := n ∪ {n}
35end

37theorem ordinal.succ.def [n : term] :
38    |- succ(n) = n ∪ {n}
39proof
40    done by eq.refl [succ(n)]
41qed

We can prove now that the result we get is still an ordinal. This proof isn't conceptually complicated but it has a few things to check.

46theorem ordinal.succ.is [α : term] : (α : Ord)
47    |- succ(α) : Ord
48proof
49    follows succ(α) = α ∪ {α} by ordinal.succ.def;
50    
51    follows transitive(succ(α)) as
52        suffices ∀x ∈ succ(α), x ⊆ succ(α) by transitive.def;
53        arbitrary x st x ∈ succ(α);
54
55        -- x is either from α or is α. split on which case we are in.
56        follows x ∈ α ∨ x = α by union.def, singleton.def given succ(α) = α ∪ {α};
57
58        cases:
59        | x ∈ α then
60            follows transitive(α) by ordinal.def given α : Ord;
61            thus x ⊆ α by transitive.def;
62            follows α ⊆ succ(α) by union.left_sub;
63            done by sub.trans
64        | x = α then 
65            done by union.left_sub given succ(α) = α ∪ {α}
66    ;
67
68    follows well_ordered(succ(α)) as
69        suffices ∀β, β ⊆ succ(α) ∧ β ≠ ∅ → ∃γ, is_least(γ, β) by well_ordered.def;
70        arbitrary β st β ⊆ succ(α) ∧ β ≠ ∅;
71
72        -- there are two cases. either β = {α} in which case α is the least
73        -- element or β ∩ α ≠ ∅ in which case we can use the well orderedness of
74        -- α to get a least element from it.
75        assume β = {α} then is_least(α, β) as
76            suffices α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ);
77            follows α ∈ β          by singleton.def given β = {α};
78            follows ¬∃γ ∈ β, γ ≠ α by singleton.def;
79            done logically
80        ;
81
82        assume β ≠ {α} then ∃γ, is_least(γ, β) as
83            -- consider only the subset of β in α
84            let β' := β ∩ α;
85            follows β' ⊆ α ∧ β' ⊆ β by inter.sub_right, inter.sub_left;
86            follows β' ≠ ∅ as 
87                obtain x st x ∈ β ∧ x ≠ α as
88                    suffices ¬∀x ∈ β, x = α logically;
89                    assume ∀x ∈ β, x = α for_contra;
90                    thus β = {α} by singleton.def, nonempty.has_element, zfc.extensionality;
91                    contradiction
92                ;
93                follows x ∈ succ(α) by sub.def given β ⊆ succ(α) and x ∈ β;
94                follows x ∈ α       by ordinal.succ.def, union.def, singleton.def;
95                thus    x ∈ β'      by inter.def given x ∈ α and x ∈ β;
96                thus    β' ≠ ∅      by nonempty.has_element;
97            ;
98            -- we get the minimal element of this subset by the well ordering of α
99            follows well_ordered(α) by ordinal.def given α : Ord;
100            obtain γ st is_least(γ, β') by well_ordered.def;
101            thus γ ∈ β' ∧ (∀δ ∈ β', δ ≠ γ → γ ∈ δ) by is_least.def;
102            -- we want that this is still the least element of β
103            suffices is_least(γ, β) logically;
104            suffices γ ∈ β ∧ (∀δ ∈ β, δ ≠ γ → γ ∈ δ) by is_least.def;
105            -- it's in β just because β' ⊆ β
106            follows γ ∈ β by sub.def given γ ∈ β' and β' ⊆ β;
107            follows ∀δ ∈ β, δ ≠ γ → γ ∈ δ as
108                arbitrary δ st δ ∈ β; assume δ ≠ γ;
109                -- any element of β is either in α or is α. split on which case.
110                follows δ ∈ α ∨ δ = α by union.def, singleton.def, sub.def
111                    given δ ∈ β and β ⊆ succ(α) and succ(α) = α ∪ {α};
112
113                cases:
114                | δ ∈ α then
115                    follows δ ∈ β' by inter.def given δ ∈ β and δ ∈ α;
116                    done given ∀δ ∈ β, δ ≠ γ → γ ∈ δ
117                | δ = α then done by sub.def given γ ∈ β' and β' ⊆ α
118            ;
119
120            done logically
121        ;
122
123        done logically
124    ;
125
126    thus succ(α) : Ord by ordinal.def given transitive(succ(α)) and well_ordered(succ(α));
127qed

Properties

8module set.ordinal.props

Returning to our characterization of ordinals as sets containing every previous ordinal, we want to prove that every element of an ordinal is an ordinal. Doing this will require several new lemmas.

First we will prove that we have the trichotomy property for members of an ordinal. We will have a stronger trichotomy on all ordinals later but since we do not yet know that the elements of an ordinal are still ordinals, we cannot apply it.

10lemma ordinal.internal_trichotomy [α β γ : term] : (α : Ord) (β ∈ α) (γ ∈ α)
11    |- γ ∈ β ∨ γ = β ∨ β ∈ γ
12proof
13    follows transitive(α) ∧ well_ordered(α) by ordinal.def;
14
15    -- The idea here is that {β, γ} ⊆ α so it must have a least element.
16    follows {β, γ} ⊆ α by pair.def, sub.def given β ∈ α and γ ∈ α;
17    follows {β, γ} ≠ ∅ by pair.non_empty;
18
19    -- the least element δ must be either β or γ
20    obtain  δ st is_least(δ, {β, γ}) by well_ordered.def given well_ordered(α);
21    follows δ ∈ {β, γ}    by is_least.def given is_least(δ, {β, γ});
22    follows δ = β ∨ δ = γ by pair.def;
23
24    -- whichever one δ is it must be either equal to or in the other
25    follows ∀η ∈ {β, γ}, η ≠ δ → δ ∈ η by is_least.def given is_least(δ, {β, γ});
26    follows ∀η ∈ {β, γ}, η = δ ∨ δ ∈ η logically;
27    follows β = δ ∨ δ ∈ β by pair.def;
28    follows γ = δ ∨ δ ∈ γ by pair.def;
29
30    -- which suffices. you can check the cases on δ = β ∨ δ = γ
31    done logically
32qed