Theorem chintcl

Description: The intersection (infimum) of a nonempty subset of CH belongs to CH . Part of Theorem 3.13 of Beran p. 108. Also part of Definition 3.4-1 in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	chintcl	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\to \bigcap A\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		inteq	$$⊢A=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \bigcap A=\bigcap if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)$$
2	1	eleq1d	$$⊢A=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left(\bigcap A\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \bigcap if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\right)$$
3		sseq1	$$⊢A=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\subseteq {\mathbf{C}}_{\mathscr{H}}\right)$$
4		neeq1	$$⊢A=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\ne \varnothing \leftrightarrow if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
5	3 4	anbi12d	$$⊢A=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\leftrightarrow \left(if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\ne \varnothing \right)\right)$$
6		sseq1	$$⊢{\mathbf{C}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{C}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\subseteq {\mathbf{C}}_{\mathscr{H}}\right)$$
7		neeq1	$$⊢{\mathbf{C}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left({\mathbf{C}}_{\mathscr{H}}\ne \varnothing \leftrightarrow if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
8	6 7	anbi12d	$$⊢{\mathbf{C}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left({\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge {\mathbf{C}}_{\mathscr{H}}\ne \varnothing \right)\leftrightarrow \left(if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\ne \varnothing \right)\right)$$
9		ssid	$$⊢{\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
10		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
11	10	ne0ii	$$⊢{\mathbf{C}}_{\mathscr{H}}\ne \varnothing$$
12	9 11	pm3.2i	$$⊢\left({\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge {\mathbf{C}}_{\mathscr{H}}\ne \varnothing \right)$$
13	5 8 12	elimhyp	$$⊢\left(if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
14	13	chintcli	$$⊢\bigcap if\left(\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{C}}_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	2 14	dedth	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\to \bigcap A\in {\mathbf{C}}_{\mathscr{H}}$$