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

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)).