forcing:solufiltroexpuni [WikiMat]

Vamos mostrar que valem as três propriedades de um filtro e teremos o resultado:

   *$[\![ \dot{G} \not= \emptyset ]\!]=1$. 
         *Sabemos que $1 \in \mathcal{A}$, assim $(\check{1},1) \in G$, com isso $[\![ \dot{G} = 1]\!]=1$ e portanto $g \not= \emptyset$, como queríamos.
   *$[\![ \forall p \in \dot{G} \,\, \forall q \in \dot{G} \Rightarrow \exists r \in \dot{G} \,\, r \leq p \land r \leq q ]\!]=1$.
         *Vamos notar que basta mostrar que $[\![ \forall p \in \dot{G} \,\, \forall q \in \dot{G}]\!] \ leq [\![\exists r \in \dot{G} \,\, r \leq p \land r \leq q ]\!]$
         *Fixemos $a,b$ quaisquer, assim $[\![ \check{a} \in \dot{G} \wedge \check{b} \in \dot{G}]\!]=[\![ \check{a} \in \dot{G}]\!][\![\check{b} \in \dot{G}]\!]=ab \leq 1$
         *$[\![\exists r \in \dot{G} \,\, r \leq p \land r \leq q ]\!] = 1$, pois $(\check{0},0) \in \dot{G}$ e para todo $a,b$, $(\check{0},0)\leq a,b$
   *$[\![ \forall p \in \dot{G} \,\, \forall q \in \check{\mathcal{A}} \,\, p \leq q \Rightarrow q \in \dot{G} ]\!]=1$.
         *Notemos que basta mostrar que $[\![ \forall p \in \dot{G} \,\, \forall q \in \check{\mathcal{A}} \,\, p\leq q ]\!] \leq  [\![ q \in \dot{G} ]\!]$
         *Fixemos $a,b \in \mathcal{A}$ quaisquer, assim $[\![ \check{a} \in \dot{G} \,\, \check{b} \in \check{\mathcal{A}} \,\, \check{a}\leq \check{b} ]\!] \leq  [\![ \check{b} \in \dot{G} ]\!]$
         * $[\![ \check{a} \in \dot{G} \,\, \check{b} \in \check{\mathcal{A}} \,\, \check{a}\leq \check{b} ]\!] = [\![\check{a} \in \dot{G} ]\!][\![ \check{b} \in \check{\mathcal{A}}]\!][\![\check{a} \leq \check{b} ]\!] = [\![\check{a} \in \dot{G} ]\!] = a \leq b = [\![\check{b} \in \dot{G} ]\!]$ <wrap right>$\square$</wrap>