mdsl1i

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdsl.1	$⊢ A \in C_{ℋ}$
	mdsl.2	$⊢ B \in C_{ℋ}$
Assertion	mdsl1i	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \leftrightarrow A 𝑀_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		mdsl.1	$⊢ A \in C_{ℋ}$
2		mdsl.2	$⊢ B \in C_{ℋ}$
3		sseq2	$⊢ x = y \lor_{ℋ} (A \cap B) \to (A \cap B \subseteq x \leftrightarrow A \cap B \subseteq y \lor_{ℋ} (A \cap B))$
4		sseq1	$⊢ x = y \lor_{ℋ} (A \cap B) \to (x \subseteq A \lor_{ℋ} B \leftrightarrow y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)$
5	3 4	anbi12d	$⊢ x = y \lor_{ℋ} (A \cap B) \to ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \leftrightarrow (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B))$
6		sseq1	$⊢ x = y \lor_{ℋ} (A \cap B) \to (x \subseteq B \leftrightarrow y \lor_{ℋ} (A \cap B) \subseteq B)$
7		oveq1	$⊢ x = y \lor_{ℋ} (A \cap B) \to x \lor_{ℋ} A = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A$
8	7	ineq1d	$⊢ x = y \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} A) \cap B = ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B$
9		oveq1	$⊢ x = y \lor_{ℋ} (A \cap B) \to x \lor_{ℋ} (A \cap B) = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)$
10	8 9	eqeq12d	$⊢ x = y \lor_{ℋ} (A \cap B) \to ((x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B) \leftrightarrow ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))$
11	6 10	imbi12d	$⊢ x = y \lor_{ℋ} (A \cap B) \to ((x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \leftrightarrow (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)))$
12	5 11	imbi12d	$⊢ x = y \lor_{ℋ} (A \cap B) \to (((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \leftrightarrow ((A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))))$
13	12	rspccv	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \to (y \lor_{ℋ} (A \cap B) \in C_{ℋ} \to ((A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))))$
14		impexp	$⊢ (((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \land y \lor_{ℋ} (A \cap B) \subseteq B) \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)) \leftrightarrow ((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)))$
15		impexp	$⊢ ((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))) \leftrightarrow (y \lor_{ℋ} (A \cap B) \in C_{ℋ} \to ((A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))))$
16	14 15	bitr2i	$⊢ (y \lor_{ℋ} (A \cap B) \in C_{ℋ} \to ((A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)))) \leftrightarrow (((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \land y \lor_{ℋ} (A \cap B) \subseteq B) \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B))$
17		inss2	$⊢ A \cap B \subseteq B$
18	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
19		chlub	$⊢ (y \in C_{ℋ} \land A \cap B \in C_{ℋ} \land B \in C_{ℋ}) \to ((y \subseteq B \land A \cap B \subseteq B) \leftrightarrow y \lor_{ℋ} (A \cap B) \subseteq B)$
20	18 2 19	mp3an23	$⊢ y \in C_{ℋ} \to ((y \subseteq B \land A \cap B \subseteq B) \leftrightarrow y \lor_{ℋ} (A \cap B) \subseteq B)$
21	20	biimpd	$⊢ y \in C_{ℋ} \to ((y \subseteq B \land A \cap B \subseteq B) \to y \lor_{ℋ} (A \cap B) \subseteq B)$
22	17 21	mpan2i	$⊢ y \in C_{ℋ} \to (y \subseteq B \to y \lor_{ℋ} (A \cap B) \subseteq B)$
23	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
24		sstr	$⊢ (y \lor_{ℋ} (A \cap B) \subseteq B \land B \subseteq A \lor_{ℋ} B) \to y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B$
25	23 24	mpan2	$⊢ y \lor_{ℋ} (A \cap B) \subseteq B \to y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B$
26	22 25	syl6	$⊢ y \in C_{ℋ} \to (y \subseteq B \to y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)$
27		chub2	$⊢ (A \cap B \in C_{ℋ} \land y \in C_{ℋ}) \to A \cap B \subseteq y \lor_{ℋ} (A \cap B)$
28	18 27	mpan	$⊢ y \in C_{ℋ} \to A \cap B \subseteq y \lor_{ℋ} (A \cap B)$
29	26 28	jctild	$⊢ y \in C_{ℋ} \to (y \subseteq B \to (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B))$
30		chjcl	$⊢ (y \in C_{ℋ} \land A \cap B \in C_{ℋ}) \to y \lor_{ℋ} (A \cap B) \in C_{ℋ}$
31	18 30	mpan2	$⊢ y \in C_{ℋ} \to y \lor_{ℋ} (A \cap B) \in C_{ℋ}$
32	29 31	jctild	$⊢ y \in C_{ℋ} \to (y \subseteq B \to (y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)))$
33	32 22	jcad	$⊢ y \in C_{ℋ} \to (y \subseteq B \to ((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \land y \lor_{ℋ} (A \cap B) \subseteq B))$
34		chjass	$⊢ (y \in C_{ℋ} \land A \cap B \in C_{ℋ} \land A \in C_{ℋ}) \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A = y \lor_{ℋ} ((A \cap B) \lor_{ℋ} A)$
35	18 1 34	mp3an23	$⊢ y \in C_{ℋ} \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A = y \lor_{ℋ} ((A \cap B) \lor_{ℋ} A)$
36	18 1	chjcomi	$⊢ (A \cap B) \lor_{ℋ} A = A \lor_{ℋ} (A \cap B)$
37	1 2	chabs1i	$⊢ A \lor_{ℋ} (A \cap B) = A$
38	36 37	eqtri	$⊢ (A \cap B) \lor_{ℋ} A = A$
39	38	oveq2i	$⊢ y \lor_{ℋ} ((A \cap B) \lor_{ℋ} A) = y \lor_{ℋ} A$
40	35 39	syl6eq	$⊢ y \in C_{ℋ} \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A = y \lor_{ℋ} A$
41	40	ineq1d	$⊢ y \in C_{ℋ} \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} A) \cap B$
42		chjass	$⊢ (y \in C_{ℋ} \land A \cap B \in C_{ℋ} \land A \cap B \in C_{ℋ}) \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B) = y \lor_{ℋ} ((A \cap B) \lor_{ℋ} (A \cap B))$
43	18 18 42	mp3an23	$⊢ y \in C_{ℋ} \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B) = y \lor_{ℋ} ((A \cap B) \lor_{ℋ} (A \cap B))$
44	18	chjidmi	$⊢ (A \cap B) \lor_{ℋ} (A \cap B) = A \cap B$
45	44	oveq2i	$⊢ y \lor_{ℋ} ((A \cap B) \lor_{ℋ} (A \cap B)) = y \lor_{ℋ} (A \cap B)$
46	43 45	syl6eq	$⊢ y \in C_{ℋ} \to (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B) = y \lor_{ℋ} (A \cap B)$
47	41 46	eqeq12d	$⊢ y \in C_{ℋ} \to (((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B) \leftrightarrow (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B))$
48	47	biimpd	$⊢ y \in C_{ℋ} \to (((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B) \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B))$
49	33 48	imim12d	$⊢ y \in C_{ℋ} \to ((((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \land (A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B)) \land y \lor_{ℋ} (A \cap B) \subseteq B) \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)) \to (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B)))$
50	16 49	syl5bi	$⊢ y \in C_{ℋ} \to ((y \lor_{ℋ} (A \cap B) \in C_{ℋ} \to ((A \cap B \subseteq y \lor_{ℋ} (A \cap B) \land y \lor_{ℋ} (A \cap B) \subseteq A \lor_{ℋ} B) \to (y \lor_{ℋ} (A \cap B) \subseteq B \to ((y \lor_{ℋ} (A \cap B)) \lor_{ℋ} A) \cap B = (y \lor_{ℋ} (A \cap B)) \lor_{ℋ} (A \cap B)))) \to (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B)))$
51	13 50	syl5com	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \to (y \in C_{ℋ} \to (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B)))$
52	51	ralrimiv	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \to \forall y \in C_{ℋ} (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B))$
53		mdbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ} B \leftrightarrow \forall y \in C_{ℋ} (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B)))$
54	1 2 53	mp2an	$⊢ A 𝑀_{ℋ} B \leftrightarrow \forall y \in C_{ℋ} (y \subseteq B \to (y \lor_{ℋ} A) \cap B = y \lor_{ℋ} (A \cap B))$
55	52 54	sylibr	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \to A 𝑀_{ℋ} B$
56		mdbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)))$
57	1 2 56	mp2an	$⊢ A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))$
58		ax-1	$⊢ (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \to ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)))$
59	58	ralimi	$⊢ \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \to \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)))$
60	57 59	sylbi	$⊢ A 𝑀_{ℋ} B \to \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)))$
61	55 60	impbii	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \to (x \subseteq B \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))) \leftrightarrow A 𝑀_{ℋ} B$

Metamath Proof Explorer

Theorem mdsl1i

Proof