285: Some Parts of Legitimate Formulas for ZFC Set Theory

<The previous article in this series | The table of contents of this series | The next article in this series>

A description/proof of some parts of legitimate formulas for ZFC set theory

---

Topics

About: set

---

The table of contents of this article

• Starting Context
• Target Context
• Orientation
• Main Body
• 1: Note
• 2: Description 1
• 3: Proof 1
• 4: Description 2
• 5: Proof 2
• 6: Description 3
• 7: Proof 3
• 8: Description 4
• 9: Proof 4
• 10: Description 5
• 11: Proof 5
• 12: Description 6
• 13: Proof 6
• 14: Description 7
• 15: Proof 7
• 16: Description 8
• 17: Proof 8
• 18: Description 9
• 19: Proof 9
• 20: Description 10
• 21: Proof 10
• 22: Description 11
• 23: Proof 11
• 24: Description 12
• 25: Proof 12
• 26: Description 13
• 27: Proof 13
• 28: Description 14
• 29: Proof 14
• 30: Description 15
• 31: Proof 15
• 32: Description 16
• 33: Proof 16
• 34: Description 17
• 35: Proof 17
• 36: Description 18
• 37: Proof 18
• 38: Description 19
• 39: Proof 19
• 40: Description 20
• 41: Proof 20
• 42: Description 21
• 43: Proof 21
• 44: Description 22
• 45: Proof 22
• 46: Description 23
• 47: Proof 23
• 48: Description 24
• 49: Proof 24
• 50: Description 25
• 51: Proof 25
• 52: Description 26
• 53: Proof 26
• 54: Description 27
• 55: Proof 27
• 56: Description 28
• 57: Proof 28
• 58: Description 29
• 59: Proof 29
• 60: Description 30
• 61: Proof 30
• 62: Description 31
• 63: Proof 31
• 64: Description 32
• 65: Proof 32
• 66: Description 33
• 67: Proof 33
• 68: Description 34
• 69: Proof 34
• 70: Description 35
• 71: Proof 35
• 72: Note

---

Starting Context

• The reader knows a definition of set.
• The reader admits the proposition that the product of any finite number of sets is a set.
• The reader admits the proposition that for any 2 sets, the collection of all the relations between the sets is a set.
• The reader admits the proposition that for any 2 sets, the collection of all the functions between the sets is a set..

---

Target Context

• The reader will have a description and a proof of the proposition that some expressions can be parts of legitimate formulas for the ZFC set theory.

---

Orientation

There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.

---

Main Body

---

1: Note

The subset axiom states that when $S$ is a set, $S_1:=\{s\in S|\varphi (s,A_1,A_2,...,A_n)\}$ is a set where $A_i$ is any set that is not $S_1$ and $\varphi$ is something called formula. The reason why $A_i$ is not allowed to be $S_1$ is that otherwise, $\varphi (s,S_1)=s\in S_1$ would be allowed, which would not really determine what would be in $S_1$. Likewise, the replacement axiom involves a formula.

Let us note that $A_i$ is externally determined, which means that $A_i$ cannot be constructed base on $s$. For example, $A_i$ cannot be like $A_2=A_1\cap s$ or $A_2=\{a\in s|a>2\}$.

Any formula in the ZFC set theory has to be legitimate, which means that the formula uses only the argument sets, some other set variables defined legitimately inside the formula, $\in ,=,\mathrm{\forall },\mathrm{\exists },\wedge ,\vee ,\mathrm{\neg },⟹,⟺$, and (~) as to avoid ambiguity, where any 'other set variable defined legitimately inside the formula' is $\mathrm{\exists }p\psi (p,...)$ or $\mathrm{\forall }p\psi (p,...)$ where $\psi (p,...)$ is a legitimate part. Let us mean by 'legitimate set variable' an argument variable or a set variable defined legitimately inside the formula, hereafter.

It is not so obvious whether an expression like '$\mathrm{\exists }pp\in \{...\}$' where $\{...\}$ is a set is a part of a legitimate formula, because $\{\}$ is not declared to be usable in legitimate formulas by definition: $\{...\}$ being a set is not enough; it has to be able to be expressed legitimately with only the certified elements.

But once an expression like $\mathrm{\exists }pp=\{...\}$, is confirmed to be legitimate, $p$ can be used representing $\{...\}$ thereafter. That is the reason why we deal with such expressions in Descriptions.

If the requirement for such a formula seems to be too restrictive (and too arbitrary), I understand that the ZFC theory is only listing what can be safely called sets, not saying that what cannot be expressed with a legitimate formula cannot be a set (there is an article that argues my thoughts on that point). Anyway, we stick to what the ZFC theory guarantees in this article.

---

2: Description 1

For any legitimate set variable, $p$, and any expression, $e$, if $p\in e$ is legitimate, $p=e$ is legitimate where $e$ is $\{s\in S|\varphi (s,...)\}$ for example.

On the other hand, if $p=e$ is legitimate, $p\in e$ is legitimate.

In fact, if $p=e$ is legitimate, $e\in p$ is legitimate.

Furthermore, if $p=e$ and $p=e^{\prime }$ are legitimate, $e\in e^{\prime }$ and $e=e^{\prime }$ are legitimate.

So, in the following Descriptions, if a 1 form is described, also the other forms ares implied, even if without being mentioned.

---

3: Proof 1

Let us suppose that $p\in e$ is legitimate. $p=e$ is $(\mathrm{\forall }{p}^{\prime }\in p,p^{\prime }\in e)\wedge (\mathrm{\forall }{p}^{\prime }\in e,p^{\prime }\in p)$, but $p^{\prime }\in e$ is a legitimate part.

Let us suppose that $p=e$ is legitimate. $p\in e$ is $\mathrm{\exists }{p}^{\prime }=e,p\in p^{\prime }$, but $p^{\prime }=e$ is a legitimate part.

Let us suppose that $p=e$ is legitimate. $e\in p$ is $\mathrm{\exists }{p}^{\prime }=e,p^{\prime }\in p$.

Let us suppose that $p=e$ and $p=e^{\prime }$ are legitimate. $e\in e^{\prime }$ is $\mathrm{\exists }p=e,\mathrm{\exists }{p}^{\prime }=e^{\prime },p\in p^{\prime }$. $e=e^{\prime }$ is $\mathrm{\exists }p=e,\mathrm{\exists }{p}^{\prime }=e^{\prime },p=p^{\prime }$.

---

4: Description 2

For any legitimate set variable, $p$, any expression, ${\varphi }_1(...)$, such that $s\in {\varphi }_1(...)$ is legitimate when $s$ is any legitimate set variable, and any legitimate expression, ${\varphi }_2(s,...)$, $p\in \{s\in {\varphi }_1(...)|{\varphi }_2(s,...)\}$ is legitimate.

---

5: Proof 2

$p\in \{s\in {\varphi }_1(...)|{\varphi }_2(s,...)\}$ is $(p\in {\varphi }_1(...))\wedge {\varphi }_2(p,...)$.

---

6: Description 3

For any legitimate set variables, $p,S_1,S_2,...,S_n$, $p\in \{S_1,S_2,...,S_n\}$ is legitimate.

---

7: Proof 3

$p\in \{S_1,S_2,...,S_n\}$ is $(p=S_1)\vee (p=S_2)\vee ...\vee (p=S_n)$.

---

8: Description 4

For any legitimate set variables, $p,S_1,S_2$, $p\in ⟨S_1,S_2⟩$ is legitimate.

---

9: Proof 4

$⟨S_1,S_2⟩$ is $\{S_1,\{S_1,S_2\}\}$. $p\in \{S_1,\{S_1,S_2\}\}$ is $(p=S_1)\vee (p=\{S_1,S_2\})$, and $p=\{S_1,S_2\}$ is legitimate by Description 3 and Description 1.

---

10: Description 5

For any legitimate set variables, $p,S$, $p\in Pow(S)$ is legitimate where $Pow(\bullet )$ means the power set of the argument.

---

11: Proof 5

$p\in Pow(S)$ is $p\subseteq S$, so, is legitimate.

---

12: Description 6

For any legitimate set variables, $p,S_1,S_2,...,S_n$, $p\in S_1\times S_2\times ...\times S_n$ is legitimate.

---

13: Proof 6

As is shown in the proof of the proposition that the product of any finite number of sets is a set, $S_1\times S_2=\{s\in Pow(Pow(S_1\cup S_2))|\mathrm{\exists }{s}_1\in S_1,\mathrm{\exists }{s}_2\in S_2,s=⟨s_1,s_2⟩\}$. But $s\in Pow(Pow(S_1\cup S_2))$ is $(\mathrm{\exists }{s}^{\prime }=Pow(S_1\cup S_2))\wedge (s\in Pow{s}^{\prime })$ and is legitimate, because $s^{\prime }=Pow(S_1\cup S_2)$ and $s\in Pow{s}^{\prime }$ are legitimate by Description 5 and Description 1. $s=⟨\bullet ,\bullet ⟩$ is legitimate by Description 4 and Description 1. Then, $p\in S_1\times S_2$ is legitimate by Description 2.

$p\in S_1\times S_2\times S_3$ is $(\mathrm{\exists }{p}^{\prime }=(S_1\times S_2))\wedge (p\in (p^{\prime }\times S_3))$, which is legitimate by the previous paragraph and Description 1, and so on.

---

14: Description 7

For any legitimate set variables, $p,S_1,S_2$, '$p$ is a relation from $S_1$ to $S_2$' is legitimate.

---

15: Proof 7

'$p$ is a relation from $S_1$ to $S_2$' is $p\in Pow(S_1\times S_2)$, which is $(\mathrm{\exists }{p}^{\prime }=S_1\times S_2)\wedge (p\in Pow{p}^{\prime })$. $p^{\prime }=S_1\times S_2$ and $p\in Pow{p}^{\prime }$ are legitimate by Descriptions 5, 6, and 1.

---

16: Description 8

For any legitimate set variables, $p,S_1,S_2$, '$p$ is a function from $S_1$ to $S_2$' is legitimate.

---

17: Proof 8

The set of all such possible functions is $F=\{f\in Pow(S_1\times S_2)|(\mathrm{\forall }{s}_1\in S_1,\mathrm{\exists }{s}_2\in S_2,⟨s_1,s_2⟩\in f)\wedge ((\mathrm{\exists }{s}_1\in S_1,\mathrm{\exists }{s}_2\in S_2,\mathrm{\exists }{s_2}^{\prime }\in S_2,(⟨s_1,s_2⟩\in f)\wedge (⟨s_1,{s_2}^{\prime }⟩\in f))⟹(s_2={s_2}^{\prime }))\}$. So, $p\in F$, which is '$p$ is a function from $S_1$ to $S_2$', is legitimate by Descriptions 1, 2, 4, 5, and 6.

---

18: Description 9

For any legitimate set variables, $p,f,S_1,S_2,S_3$, where $f$ is a function, $f:S_1\to S_2$, $p\in f|S_3$, where $f|S_3$ is the restriction of $f$, is legitimate.

---

19: Proof 9

$f{|}_{S_3}=\{s\in f|\mathrm{\exists }{s}_3\in S_3,\mathrm{\exists }{s}_2\in S_2,s=⟨s_3,s_2⟩\}$. So, $p\in f|S_3$ is legitimate by Descriptions 1, 2, and 4.

---

20: Description 10

For any legitimate set variables, $p,f,S$, where $f$ is a function, $p=f(S)$ is legitimate when $S$ is a member of the domain of $f$.

---

21: Proof 10

$p=f(S)$ is $\mathrm{\exists }{p}^{\prime }\in f,p^{\prime }=⟨S,p⟩$, which is legitimate by Descriptions 1 and 4.

---

22: Description 11

For any legitimate set variables, $p,S$, and any ordering, $<$, that can apply to $p$ and $S$, $p<S$ or $p\le S$ is legitimate, if the ordering is legitimately defined, which means that as the ordering is really a relation, which is a set, the relation has to be able to be expressed as a legitimate set variable.

---

23: Proof 11

As $<$ is really a relation, $R$, $p<S$ or $p\le S$ is $⟨p,S⟩\in R$ or $⟨p,S⟩\in R\vee p=S$, respectively, which is legitimate by Description 4.

---

24: Description 12

For any legitimate set variables, $p,f$, where $f$ is a function, $p\in img(f)$ is legitimate where $img(\bullet )$ is the image of the argument.

---

25: Proof 12

$p\in img(f)$ is $\mathrm{\exists }{p}^{\prime },⟨p^{\prime },p⟩\in f$, which is legitimate by Description 4.

---

26: Description 13

For any legitimate set variables, $p,f$, where $f$ is a function, $p\in dom(f)$ is legitimate where $dom(\bullet )$ is the domain of the argument.

---

27: Proof 13

$p\in dom(f)$ is $\mathrm{\exists }{p}^{\prime },⟨p,p^{\prime }⟩\in f$, which is legitimate by Description 4.

---

28: Description 14

For any legitimate set variables, $p,S,s$, where $s\in S$, and any ordering, $<$, $p\in seg(S,<,s)$, which is the initial segment of $S$ with respect to $<$ and $s$, is legitimate.

---

29: Proof 14

$p\in seg(S,<,s)$ is $p\in \{p^{\prime }\in S|p^{\prime }<s\}$, which is legitimate by Descriptions 2 and 11.

---

30: Description 15

For any legitimate set variables, $<,S$, '$<$ is a linear ordering on $S$' is legitimate.

---

31: Proof 15

'$<$ is a linear ordering on $S$' is $<\in Pow(S\times S)\wedge \mathrm{\forall }{s}_1,s_2,s_3\in S(⟨s_1,s_2⟩\in <\wedge ⟨s_2,s_3⟩\in <)⟨s_1,s_3⟩\in <\wedge \mathrm{\forall }{s}_1\in S,⟨s_1,s_1⟩\notin <\wedge \mathrm{\forall }{s}_1\in S(\mathrm{\forall }{s}_2\in S,\mathrm{\neg }{s}_1=s_2)((⟨s_1,s_2⟩\in <\vee ⟨s_2,s_1⟩\in <)\wedge \mathrm{\neg }(⟨s_1,s_2⟩\in <\wedge ⟨s_2,s_1⟩\in <))$.

---

32: Description 16

For any legitimate set variables, $<,S$, '$<$ is a well-ordering on $S$' is legitimate.

---

33: Proof 16

'$<$ is a well-ordering on $S$' is '$<$ is a linear ordering on $S$' $\wedge \mathrm{\forall }{S}^{\prime }\subseteq S(\mathrm{\exists }m\in S^{\prime }(\mathrm{\forall }s\in S^{\prime },(\mathrm{\neg }m=s),⟨m,s⟩\in <)$.

---

34: Description 17

For any legitimate set variables, $f,S_1,S_2$, '$f$ is an injective function from $S_1$ into $S_2$' is legitimate.

---

35: Proof 17

'$f$ is an injective function from $S_1$ into $S_2$' is '$f$ is an function from $S_1$ into $S_2$' $\wedge (\mathrm{\forall }{p}_1\in S_1(\mathrm{\forall }{p}_2\in S_1,\mathrm{\neg }{p}_2=p_1)(\mathrm{\exists }{p}_3\in S_2,⟨p_1,p_3⟩\in f,\mathrm{\exists }{p}_4\in S_2,⟨p_2,p_4⟩\in f,\mathrm{\neg }{p}_3=p_4))$. Note that as the condition that $f$ is a function is in place, it is guaranteed that there are unique $p_3$ and $p_4$, so, if the found $p_3$ and $p_4$ satisfy $\mathrm{\neg }{p}_3=p_4$, it will be OK.

---

36: Description 18

For any legitimate set variables, $f,S_1,S_2$, '$f$ is a surjective function from $S_1$ onto $S_2$' is legitimate.

---

37: Proof 18

'$f$ is an surjective function from $S_1$ onto $S_2$' is '$f$ is an function from $S_1$ into $S_2$' $\wedge \mathrm{\forall }{p}_2\in S_2,\mathrm{\exists }{p}_1\in S_1,⟨p_1,p_2⟩\in f$.

---

38: Description 19

For any legitimate set variables, $f,S_1,S_2$, '$f$ is a bijective function from $S_1$ onto $S_2$' is legitimate.

---

39: Proof 19

'$f$ is a bijective function from $S_1$ onto $S_2$' is '$f$ is an injective function from $S_1$ into $S_2$' $\wedge$ '$f$ is a surjective function from $S_1$ onto $S_2$'.

---

40: Description 20

For any legitimate set variables, $p,S$, '$p$ is equinumerous with $S$', denoted as $p\approx S$, is legitimate.

---

41: Proof 20

$p\approx S$ is '$\mathrm{\exists }{p}^{\prime },p^{\prime }$ is a bijective function from $p$ onto $S$'.

---

42: Description 21

For any legitimate set variable, $p$, '$p$ is an ordinal number' is legitimate.

---

43: Proof 21

'$p$ is an ordinal number' is $\mathrm{\exists }S\mathrm{\exists }<$, '$<$ is a well-ordering on $S$', '$p$ is the $ϵ$-image of $(S,<)$'. '$p$ is the $ϵ$-image of $(S,<)$' is $\mathrm{\exists }{S}_1(\mathrm{\exists }f$, '$f$ is a function from $S$ to $S_1$', $\mathrm{\forall }s\in S,f(s)=\{s^{\prime }\in S_1|\mathrm{\exists }{s}^{″}<s,s^{\prime }=f(s^{″})\})$ $p=imgf$.

---

44: Description 22

For any legitimate set variables, $p,S$, '$p$ is a cardinal number of $S$' is legitimate.

---

45: Proof 22

'$p$ is a cardinal number of $S$' is '$p$ is the least ordinal number equinumerous to $S$', which is '$p$ is an ordinal number' $\wedge$ $p\approx S$ $\wedge (\mathrm{\forall }{p}^{\prime }{,}^{\prime }{p}^{\prime }$ is an ordinal number' $p^{\prime }\approx S,\mathrm{\neg }{p}^{\prime }=p)p<p^{\prime }$.

---

46: Description 23

For any legitimate set variable, $p$, '$p$ is a cardinal number' is legitimate.

---

47: Proof 23

'$p$ is a cardinal number' is $\mathrm{\exists }S{,}^{\prime }p$ is a cardinal number of $S$'.

---

48: Description 24

For any legitimate set variable, $S$, and any net, $n:D\to T$ where $D$ is any directed set and $T$ is any topological space, '$n$ is frequently in $S$' is legitimate.

---

49: Proof 24

'$n$ is frequently in $S$' is $\mathrm{\forall }d\in D(\mathrm{\exists }{d}^{\prime }\in D,d\le d^{\prime })n(d^{\prime })\in S$.

---

50: Description 25

For any legitimate set variable, $S$, and any net, $n:D\to T$ where $D$ is any directed set and $T$ is any topological space, '$n$ is eventually in $S$' is legitimate.

---

51: Proof 25

'$n$ is eventually in $S$' is $\mathrm{\exists }d\in D(\mathrm{\forall }{d}^{\prime }\in D,d\le d^{\prime })n(d^{\prime })\in S$.

---

52: Description 26

For any legitimate set variables, $p,S_1,S_2,...,S_n$, $p\in S_1\cup S_2\cup ...\cup S_n$ is legitimate.

---

53: Proof 26

'$p\in S_1\cup S_2\cup ...\cup S_n$' is '$p\in S_1\vee p\in S_2\vee ...\vee p\in S_n$'.

---

54: Description 27

For any legitimate set variables, $p,S$, and any legitimate function variable, $f$, '$p\in {\cup }_{\mathrm{\forall }s\in S}f(s)$' is legitimate.

---

55: Proof 27

'$p\in {\cup }_{\mathrm{\forall }s\in S}f(s)$' is '$\mathrm{\exists }s\in S,p\in f(s)$'.

---

56: Description 28

For any legitimate set variable, $p$, and any ordinal number variable, $o$, $p\in V_o$, where $V_o$ means the set of sets defined by $V_0=\mathrm{\varnothing },V_o={\cup }_{o^{\prime }\in o}Pow{V}_{o^{\prime }}$, is legitimate.

---

57: Proof 28

'$p\in V_o$' is '$\mathrm{\exists }\delta {,}^{\prime }\delta \text{ is an ordinal number' },o\in \delta ,\mathrm{\exists }S\mathrm{\exists }V{,}^{\prime }\text{V is a function from }\delta \text{ to }{S}^{\prime },\mathrm{\forall }\alpha \in \delta ,V(\alpha )={\cup }_{{\alpha }^{\prime }\in \alpha }PowV({\alpha }^{\prime }),p\in V(o)$'.

---

58: Description 29

For any legitimate set variable, $p$, '$p$ is grounded' is legitimate.

---

59: Proof 29

'$p$ is grounded' is '$\mathrm{\exists }o,o\text{ is an ordinal number },p\subseteq V_o$'.

---

60: Description 30

For any legitimate set variables, $p,S$, '$p=rankS$' is legitimate.

---

61: Proof 30

'$p=rankS$' is '$p\text{ is an ordinal number }\wedge S\subseteq V_p\wedge \mathrm{\neg }(\mathrm{\exists }o\in p,S\subseteq V_o)$'.

---

62: Description 31

For any legitimate set variables, $p,S$, '$p\notin S$' is legitimate.

---

63: Proof 31

'$p\notin S$' is '$\mathrm{\neg }p\in S$'.

---

64: Description 32

For any legitimate set variable, $S$, '$S$ is an open interval on $\mathbb{R}$' is legitimate.

---

65: Proof 32

'$S$ is an open interval on $\mathbb{R}$' is '$\mathrm{\exists }{p}_1,p_2(p_1,p_2\in \mathbb{R}\wedge p_1,p_2\notin S\wedge p_1\le p_2\wedge \mathrm{\forall }{p}_3\in \mathbb{R}(p_3\in S⟺p_1<p_3<p_2))$'.

---

66: Description 33

For any legitimate set variable, $S$, '$S$ is a closed interval on $\mathbb{R}$' is legitimate.

---

67: Proof 33

'$S$ is a closed interval on $\mathbb{R}$' is '$\mathrm{\exists }{p}_1,p_2(p_1,p_2\in \mathbb{R}\wedge p_1,p_2\in S\wedge p_1\le p_2\wedge \mathrm{\forall }{p}_3\in \mathbb{R}(p_3\in S⟺p_1\le p_3\le p_2))$'.

---

68: Description 34

For any legitimate set variable, $S$, '$S$ is a left-open-right-closed interval on $\mathbb{R}$' is legitimate.

---

69: Proof 34

'$S$ is a left-open-right-closed interval on $\mathbb{R}$' is '$\mathrm{\exists }{p}_1,p_2(p_1,p_2\in \mathbb{R}\wedge p_1\notin S\wedge p_2\in S\wedge p_1\le p_2\wedge \mathrm{\forall }{p}_3\in \mathbb{R}(p_3\in S⟺p_1<p_3\le p_2))$'.

---

70: Description 35

For any legitimate set variable, $S$, '$S$ is a left-closed-right-open interval on $\mathbb{R}$' is legitimate.

---

71: Proof 35

'$S$ is a left-closed-right-open interval on $\mathbb{R}$' is '$\mathrm{\exists }{p}_1,p_2(p_1,p_2\in \mathbb{R}\wedge p_1\in S\wedge p_2\notin S\wedge p_1\le p_2\wedge \mathrm{\forall }{p}_3\in \mathbb{R}(p_3\in S⟺p_1\le p_3<p_2))$'.

---

72: Note

All the text books I have read (I do not say all the text books in the world) is like "Any formula has to be legitimate." and begin to present formulas that are not so obvious how they are legitimate, at least for me. For example, they begin to use $\{...\}$ which is not any elementary component.

So, I had to list what compounds could be safely used in legitimate formulas.

Of course, those listed above are only what I have particularly noticed so far.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>