Metamath Proof Explorer

Theorem cvdmd

Description: The covering property implies the dual modular pair property. Lemma 7.5.2 of MaedaMaeda p. 31. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	cvdmd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land B ⋖_{ℋ} (A \lor_{ℋ} B)) \to A 𝑀_{ℋ}^{*} B$

Proof

Step	Hyp	Ref	Expression
1		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
2		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
3		cvmd	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ} \land (⊥ (A) \cap ⊥ (B)) ⋖_{ℋ} ⊥ (B)) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B)$
4	3	3expia	$⊢ (⊥ (A) \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to ((⊥ (A) \cap ⊥ (B)) ⋖_{ℋ} ⊥ (B) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
5	1 2 4	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((⊥ (A) \cap ⊥ (B)) ⋖_{ℋ} ⊥ (B) \to ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
6		simpr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to B \in C_{ℋ}$
7		chjcl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} B \in C_{ℋ}$
8		cvcon3	$⊢ (B \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ}) \to (B ⋖_{ℋ} (A \lor_{ℋ} B) \leftrightarrow ⊥ (A \lor_{ℋ} B) ⋖_{ℋ} ⊥ (B))$
9	6 7 8	syl2anc	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B ⋖_{ℋ} (A \lor_{ℋ} B) \leftrightarrow ⊥ (A \lor_{ℋ} B) ⋖_{ℋ} ⊥ (B))$
10		chdmj1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \lor_{ℋ} B) = ⊥ (A) \cap ⊥ (B)$
11	10	breq1d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (A \lor_{ℋ} B) ⋖_{ℋ} ⊥ (B) \leftrightarrow (⊥ (A) \cap ⊥ (B)) ⋖_{ℋ} ⊥ (B))$
12	9 11	bitrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B ⋖_{ℋ} (A \lor_{ℋ} B) \leftrightarrow (⊥ (A) \cap ⊥ (B)) ⋖_{ℋ} ⊥ (B))$
13		dmdmd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow ⊥ (A) 𝑀_{ℋ} ⊥ (B))$
14	5 12 13	3imtr4d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B ⋖_{ℋ} (A \lor_{ℋ} B) \to A 𝑀_{ℋ}^{*} B)$
15	14	3impia	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land B ⋖_{ℋ} (A \lor_{ℋ} B)) \to A 𝑀_{ℋ}^{*} B$