dmdbr2

Description: Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr . (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	dmdbr2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$

Proof

Step	Hyp	Ref	Expression
1		dmdbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)))$
2		chincl	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to x \cap A \in C_{ℋ}$
3	2	ancoms	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to x \cap A \in C_{ℋ}$
4	3	adantlr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to x \cap A \in C_{ℋ}$
5		simplr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to B \in C_{ℋ}$
6		simpr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to x \in C_{ℋ}$
7		inss1	$⊢ x \cap A \subseteq x$
8		chlub	$⊢ (x \cap A \in C_{ℋ} \land B \in C_{ℋ} \land x \in C_{ℋ}) \to ((x \cap A \subseteq x \land B \subseteq x) \leftrightarrow (x \cap A) \lor_{ℋ} B \subseteq x)$
9	8	biimpd	$⊢ (x \cap A \in C_{ℋ} \land B \in C_{ℋ} \land x \in C_{ℋ}) \to ((x \cap A \subseteq x \land B \subseteq x) \to (x \cap A) \lor_{ℋ} B \subseteq x)$
10	7 9	mpani	$⊢ (x \cap A \in C_{ℋ} \land B \in C_{ℋ} \land x \in C_{ℋ}) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B \subseteq x)$
11	4 5 6 10	syl3anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B \subseteq x)$
12		simpll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to A \in C_{ℋ}$
13		inss2	$⊢ x \cap A \subseteq A$
14		chlej1	$⊢ ((x \cap A \in C_{ℋ} \land A \in C_{ℋ} \land B \in C_{ℋ}) \land x \cap A \subseteq A) \to (x \cap A) \lor_{ℋ} B \subseteq A \lor_{ℋ} B$
15	13 14	mpan2	$⊢ (x \cap A \in C_{ℋ} \land A \in C_{ℋ} \land B \in C_{ℋ}) \to (x \cap A) \lor_{ℋ} B \subseteq A \lor_{ℋ} B$
16	4 12 5 15	syl3anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (x \cap A) \lor_{ℋ} B \subseteq A \lor_{ℋ} B$
17	11 16	jctird	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (B \subseteq x \to ((x \cap A) \lor_{ℋ} B \subseteq x \land (x \cap A) \lor_{ℋ} B \subseteq A \lor_{ℋ} B))$
18		ssin	$⊢ ((x \cap A) \lor_{ℋ} B \subseteq x \land (x \cap A) \lor_{ℋ} B \subseteq A \lor_{ℋ} B) \leftrightarrow (x \cap A) \lor_{ℋ} B \subseteq x \cap (A \lor_{ℋ} B)$
19	17 18	imbitrdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (B \subseteq x \to (x \cap A) \lor_{ℋ} B \subseteq x \cap (A \lor_{ℋ} B))$
20		eqss	$⊢ (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B) \leftrightarrow ((x \cap A) \lor_{ℋ} B \subseteq x \cap (A \lor_{ℋ} B) \land x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B)$
21	20	baib	$⊢ (x \cap A) \lor_{ℋ} B \subseteq x \cap (A \lor_{ℋ} B) \to ((x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B) \leftrightarrow x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B)$
22	19 21	syl6	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (B \subseteq x \to ((x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B) \leftrightarrow x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$
23	22	pm5.74d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \leftrightarrow (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$
24	23	ralbidva	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (B \subseteq x \to (x \cap A) \lor_{ℋ} B = x \cap (A \lor_{ℋ} B)) \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$
25	1 24	bitrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$

Metamath Proof Explorer

Theorem dmdbr2

Proof