Theorem chrelati

Description: The Hilbert lattice is relatively atomic. Remark 2 of Kalmbach p. 149. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chpssat.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	chpssat.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chrelati	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chpssat.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chpssati	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$
4		ancom	$$⊢\left(x\subseteq B\wedge \neg x\subseteq A\right)\leftrightarrow \left(\neg x\subseteq A\wedge x\subseteq B\right)$$
5		pssss	$$⊢A\subset B\to A\subseteq B$$
6		atelch	$$⊢x\in \mathrm{HAtoms}\to x\in {\mathbf{C}}_{\mathscr{H}}$$
7		chnle	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\neg x\subseteq A\leftrightarrow A\subset A{\vee }_{\mathscr{H}}x\right)$$
8	1 7	mpan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\neg x\subseteq A\leftrightarrow A\subset A{\vee }_{\mathscr{H}}x\right)$$
9	8	adantl	$$⊢\left(A\subseteq B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\neg x\subseteq A\leftrightarrow A\subset A{\vee }_{\mathscr{H}}x\right)$$
10		ibar	$$⊢A\subseteq B\to \left(x\subseteq B\leftrightarrow \left(A\subseteq B\wedge x\subseteq B\right)\right)$$
11		chlub	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq B\wedge x\subseteq B\right)\leftrightarrow A{\vee }_{\mathscr{H}}x\subseteq B\right)$$
12	1 2 11	mp3an13	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\subseteq B\wedge x\subseteq B\right)\leftrightarrow A{\vee }_{\mathscr{H}}x\subseteq B\right)$$
13	10 12	sylan9bb	$$⊢\left(A\subseteq B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\leftrightarrow A{\vee }_{\mathscr{H}}x\subseteq B\right)$$
14	9 13	anbi12d	$$⊢\left(A\subseteq B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(\neg x\subseteq A\wedge x\subseteq B\right)\leftrightarrow \left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)\right)$$
15	5 6 14	syl2an	$$⊢\left(A\subset B\wedge x\in \mathrm{HAtoms}\right)\to \left(\left(\neg x\subseteq A\wedge x\subseteq B\right)\leftrightarrow \left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)\right)$$
16	4 15	bitrid	$$⊢\left(A\subset B\wedge x\in \mathrm{HAtoms}\right)\to \left(\left(x\subseteq B\wedge \neg x\subseteq A\right)\leftrightarrow \left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)\right)$$
17	16	rexbidva	$$⊢A\subset B\to \left(\exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)\leftrightarrow \exists x\in \mathrm{HAtoms}\left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)\right)$$
18	3 17	mpbid	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(A\subset A{\vee }_{\mathscr{H}}x\wedge A{\vee }_{\mathscr{H}}x\subseteq B\right)$$