Theorem chsup0

Description: The supremum of the empty set. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	chsup0	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left\{0_{\mathscr{H}}\right\}$$
2		0ss	$$⊢\varnothing \subseteq {\mathbf{C}}_{\mathscr{H}}$$
3		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
4		snssi	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\to \left\{0_{\mathscr{H}}\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
5	3 4	ax-mp	$$⊢\left\{0_{\mathscr{H}}\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
6		chsupss	$$⊢\left(\varnothing \subseteq {\mathbf{C}}_{\mathscr{H}}\wedge \left\{0_{\mathscr{H}}\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\varnothing \subseteq \left\{0_{\mathscr{H}}\right\}\to {\bigvee }_{\mathscr{H}}\left(\varnothing \right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{0_{\mathscr{H}}\right\}\right)\right)$$
7	2 5 6	mp2an	$$⊢\varnothing \subseteq \left\{0_{\mathscr{H}}\right\}\to {\bigvee }_{\mathscr{H}}\left(\varnothing \right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{0_{\mathscr{H}}\right\}\right)$$
8	1 7	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{0_{\mathscr{H}}\right\}\right)$$
9		chsupsn	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{0_{\mathscr{H}}\right\}\right)=0_{\mathscr{H}}$$
10	3 9	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{0_{\mathscr{H}}\right\}\right)=0_{\mathscr{H}}$$
11	8 10	sseqtri	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)\subseteq 0_{\mathscr{H}}$$
12		chsupcl	$$⊢\varnothing \subseteq {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\varnothing \right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	2 12	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	13	chle0i	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)\subseteq 0_{\mathscr{H}}\leftrightarrow {\bigvee }_{\mathscr{H}}\left(\varnothing \right)=0_{\mathscr{H}}$$
15	11 14	mpbi	$$⊢{\bigvee }_{\mathscr{H}}\left(\varnothing \right)=0_{\mathscr{H}}$$