dmdbr5

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dmdbr4	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
2		chub1	$⊢ (x \in C_{ℋ} \land B \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} B$
3	2	ancoms	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} B$
4		ssin	$⊢ (x \subseteq x \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \leftrightarrow x \subseteq (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)$
5		sstr2	$⊢ x \subseteq (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
6	4 5	sylbi	$⊢ (x \subseteq x \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \to ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
7	3 6	sylan	$⊢ ((B \in C_{ℋ} \land x \in C_{ℋ}) \land x \subseteq A \lor_{ℋ} B) \to ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
8	7	ex	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to (x \subseteq A \lor_{ℋ} B \to ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
9	8	com23	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
10	9	ralimdva	$⊢ B \in C_{ℋ} \to (\forall x \in C_{ℋ} (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to \forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
11	10	adantl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \to \forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
12	1 11	sylbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \to \forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
13		sseq1	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to (x \subseteq A \lor_{ℋ} B \leftrightarrow (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B)$
14		id	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)$
15		oveq1	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to x \lor_{ℋ} B = ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B$
16	15	ineq1d	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to (x \lor_{ℋ} B) \cap A = (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A$
17	16	oveq1d	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B$
18	14 17	sseq12d	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to (x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \leftrightarrow (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
19	13 18	imbi12d	$⊢ x = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to ((x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \leftrightarrow ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
20	19	rspccv	$⊢ \forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
21		chjcl	$⊢ (y \in C_{ℋ} \land B \in C_{ℋ}) \to y \lor_{ℋ} B \in C_{ℋ}$
22	21	ancoms	$⊢ (B \in C_{ℋ} \land y \in C_{ℋ}) \to y \lor_{ℋ} B \in C_{ℋ}$
23	22	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to y \lor_{ℋ} B \in C_{ℋ}$
24		chjcl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} B \in C_{ℋ}$
25	24	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to A \lor_{ℋ} B \in C_{ℋ}$
26		chincl	$⊢ (y \lor_{ℋ} B \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ}) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ}$
27	23 25 26	syl2anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ}$
28		inss2	$⊢ (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B$
29		pm2.27	$⊢ (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
30	28 29	mpii	$⊢ (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
31	27 30	syl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
32		chub2	$⊢ (B \in C_{ℋ} \land y \in C_{ℋ}) \to B \subseteq y \lor_{ℋ} B$
33	32	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to B \subseteq y \lor_{ℋ} B$
34		chub2	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ}) \to B \subseteq A \lor_{ℋ} B$
35	34	ancoms	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to B \subseteq A \lor_{ℋ} B$
36	35	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to B \subseteq A \lor_{ℋ} B$
37	33 36	ssind	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to B \subseteq (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)$
38		simplr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to B \in C_{ℋ}$
39		chlejb2	$⊢ (B \in C_{ℋ} \land (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ}) \to (B \subseteq (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \leftrightarrow ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B))$
40	38 27 39	syl2anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (B \subseteq (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \leftrightarrow ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B))$
41	37 40	mpbid	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B = (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)$
42	41	ineq1d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A = ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap A$
43		inass	$⊢ ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap A = (y \lor_{ℋ} B) \cap ((A \lor_{ℋ} B) \cap A)$
44		incom	$⊢ (A \lor_{ℋ} B) \cap A = A \cap (A \lor_{ℋ} B)$
45		chabs2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \cap (A \lor_{ℋ} B) = A$
46	44 45	eqtrid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \lor_{ℋ} B) \cap A = A$
47	46	ineq2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (y \lor_{ℋ} B) \cap ((A \lor_{ℋ} B) \cap A) = (y \lor_{ℋ} B) \cap A$
48	43 47	eqtrid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap A = (y \lor_{ℋ} B) \cap A$
49	48	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap A = (y \lor_{ℋ} B) \cap A$
50	42 49	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A = (y \lor_{ℋ} B) \cap A$
51	50	oveq1d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B = ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B$
52	51	sseq2d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B \leftrightarrow (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
53	31 52	sylibd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
54	53	ex	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (y \in C_{ℋ} \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
55	54	com23	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \in C_{ℋ} \to ((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq A \lor_{ℋ} B \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((((y \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \lor_{ℋ} B) \cap A) \lor_{ℋ} B)) \to (y \in C_{ℋ} \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
56	20 55	syl5	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \to (y \in C_{ℋ} \to (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$
57	56	ralrimdv	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \to \forall y \in C_{ℋ} (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
58		dmdbr4	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall y \in C_{ℋ} (y \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \subseteq ((y \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
59	57 58	sylibrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \to A 𝑀_{ℋ}^{*} B)$
60	12 59	impbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B))$

Metamath Proof Explorer

Theorem dmdbr5

Proof