This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjoml6i

Description: An equivalent of the orthomodular law. Theorem 29.13(e) of MaedaMaeda p. 132. (Contributed by NM, 30-May-2004) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pjoml2.1	$⊢ A \in C_{ℋ}$
		pjoml2.2	$⊢ B \in C_{ℋ}$
	Assertion	pjoml6i	$⊢ A \subseteq B \to \exists x \in C_{ℋ} (A \subseteq ⊥ (x) \land A \lor_{ℋ} x = B)$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
4	3 2	chincli	$⊢ ⊥ (A) \cap B \in C_{ℋ}$
5	1 2	pjoml2i	$⊢ A \subseteq B \to A \lor_{ℋ} (⊥ (A) \cap B) = B$
6	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
7	1 6	chub1i	$⊢ A \subseteq A \lor_{ℋ} ⊥ (B)$
8	1 2	chdmm2i	$⊢ ⊥ (⊥ (A) \cap B) = A \lor_{ℋ} ⊥ (B)$
9	7 8	sseqtrri	$⊢ A \subseteq ⊥ (⊥ (A) \cap B)$
10	5 9	jctil	$⊢ A \subseteq B \to (A \subseteq ⊥ (⊥ (A) \cap B) \land A \lor_{ℋ} (⊥ (A) \cap B) = B)$
11		fveq2	$⊢ x = ⊥ (A) \cap B \to ⊥ (x) = ⊥ (⊥ (A) \cap B)$
12	11	sseq2d	$⊢ x = ⊥ (A) \cap B \to (A \subseteq ⊥ (x) \leftrightarrow A \subseteq ⊥ (⊥ (A) \cap B))$
13		oveq2	$⊢ x = ⊥ (A) \cap B \to A \lor_{ℋ} x = A \lor_{ℋ} (⊥ (A) \cap B)$
14	13	eqeq1d	$⊢ x = ⊥ (A) \cap B \to (A \lor_{ℋ} x = B \leftrightarrow A \lor_{ℋ} (⊥ (A) \cap B) = B)$
15	12 14	anbi12d	$⊢ x = ⊥ (A) \cap B \to ((A \subseteq ⊥ (x) \land A \lor_{ℋ} x = B) \leftrightarrow (A \subseteq ⊥ (⊥ (A) \cap B) \land A \lor_{ℋ} (⊥ (A) \cap B) = B))$
16	15	rspcev	$⊢ (⊥ (A) \cap B \in C_{ℋ} \land (A \subseteq ⊥ (⊥ (A) \cap B) \land A \lor_{ℋ} (⊥ (A) \cap B) = B)) \to \exists x \in C_{ℋ} (A \subseteq ⊥ (x) \land A \lor_{ℋ} x = B)$
17	4 10 16	sylancr	$⊢ A \subseteq B \to \exists x \in C_{ℋ} (A \subseteq ⊥ (x) \land A \lor_{ℋ} x = B)$