Proof of Events of a Probability Space: Subsets of Ω, Real Probabilities, Complements and Tail Unions

Throughout, lemmas stated over the earlier notions of $\sigma$-algebra, measure and probability space apply to $(\Omega,\mathcal{F},P)$, since these notions agree with the new ones (The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii)).

Sketch. $P$ is a finite measure on $(\Omega,\mathcal{F})$ with $P(\Omega)=1$, by A Probability Measure Is Finite (ii) and Probability Spaces, Events and Random Elements (i).

For (i): $\mathcal{F}$ is a subset of the power set of $\Omega$ by σ-Algebra and Measurable Space (i).

For (ii): as $E\subseteq\Omega$ by (i), $\Omega\in\mathcal{F}$ (σ-Algebra and Measurable Space (i)) and $P(\Omega)<\infty$, Basic Properties of a Measure (iv) gives $P(E)\in\mathbb{R}$. Also $P(E)\in[0,\infty]$ by Measure, Measure Space, and Probability Measure (i), so $0\le P(E)$ in $\mathbb{R}$ by The Extended Real Line, Its Order, and [0,∞] (ii); and $P(E)\le P(\Omega)=1$ by Basic Properties of a Measure (iii), an inequality in $\mathbb{R}$ by The Extended Real Line, Its Order, and [0,∞] (iii). These are $0\le p$ and $p\le1$ in $\mathrm{Real}$ by The Real Numbers as a Type (ii).

For (iii): $\Omega\setminus E\in\mathcal{F}$ by σ-Algebra and Measurable Space (i), and $P(\Omega\setminus E)$ (real by (ii) applied to $\Omega\setminus E$) satisfies $P(\Omega\setminus E)=P(\Omega)-P(E)=1-P(E)$, the difference in $\mathbb{R}$, by Basic Properties of a Measure (v). By Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i) this is the set of $1-p$ in $\mathrm{Real}$, so $q=1-p$.

For (iv): the membership condition is the defining property of $T_{n}$ (Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i)). Let $I_{n}=\{k\in\mathbb{N}:n\le k\}$, a subset of $\mathbb{N}$ and hence countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (i) and Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (iv). By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix), the restriction of $k\mapsto A_{k}$ to $I_{n}$ is a map $I_{n}\to\mathcal{F}$ with values $A_{k}$, and by Indexed Families of Sets and Their Union, Intersection and Product (ii) its union has the same elements as $T_{n}$; so $T_{n}$ is this union and lies in $\mathcal{F}$ by Unions and Intersections over a Countable Index Set in a σ-Algebra (i). If $m\le n$ and $n\le k$, then $m\le k$ by transitivity (Order and Arithmetic of ℕ₀ in Flat Form (i)), which gives $T_{n}\subseteq T_{m}$. Finally, as $T_{n}\in\mathcal{F}$ for every $n\in\mathbb{N}$, Maps and Relations Given by Formulas (i) gives the map $\mathbb{N}\to\mathcal{F}$, $n\mapsto T_{n}$, a sequence in $\mathcal{F}$.

For (v): the membership condition is the defining property of $L$. Let $(T_{n})$ be the sequence of (iv). A set $\omega$ lies in the intersection $\bigcap_{n\in\mathbb{N}}T_{n}$ if and only if $\omega\in T_{n}$ for every $n\in\mathbb{N}$; then $\omega\in T_{1}$, so $\omega\in A_{k}\subseteq\Omega$ for some $k$, by (i). Hence $L=\bigcap_{n\in\mathbb{N}}T_{n}$, which lies in $\mathcal{F}$ by Unions and Intersections over a Countable Index Set in a σ-Algebra (ii), since $\mathbb{N}$ is countable (Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (i)) and nonempty ($1\in\mathbb{N}$, The Set of Natural Numbers and the Number One (ii)).