mdsl2i

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, 28-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		mdsl.1	$⊢ A \in C_{ℋ}$
2		mdsl.2	$⊢ B \in C_{ℋ}$
3		chub1	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} A$
4	1 3	mpan2	$⊢ x \in C_{ℋ} \to x \subseteq x \lor_{ℋ} A$
5		iba	$⊢ x \subseteq B \to (x \subseteq x \lor_{ℋ} A \leftrightarrow (x \subseteq x \lor_{ℋ} A \land x \subseteq B))$
6		ssin	$⊢ (x \subseteq x \lor_{ℋ} A \land x \subseteq B) \leftrightarrow x \subseteq (x \lor_{ℋ} A) \cap B$
7	5 6	syl6bb	$⊢ x \subseteq B \to (x \subseteq x \lor_{ℋ} A \leftrightarrow x \subseteq (x \lor_{ℋ} A) \cap B)$
8	4 7	syl5ibcom	$⊢ x \in C_{ℋ} \to (x \subseteq B \to x \subseteq (x \lor_{ℋ} A) \cap B)$
9		chub2	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to A \subseteq x \lor_{ℋ} A$
10	1 9	mpan	$⊢ x \in C_{ℋ} \to A \subseteq x \lor_{ℋ} A$
11	10	ssrind	$⊢ x \in C_{ℋ} \to A \cap B \subseteq (x \lor_{ℋ} A) \cap B$
12	8 11	jctird	$⊢ x \in C_{ℋ} \to (x \subseteq B \to (x \subseteq (x \lor_{ℋ} A) \cap B \land A \cap B \subseteq (x \lor_{ℋ} A) \cap B))$
13		chjcl	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to x \lor_{ℋ} A \in C_{ℋ}$
14	1 13	mpan2	$⊢ x \in C_{ℋ} \to x \lor_{ℋ} A \in C_{ℋ}$
15		chincl	$⊢ (x \lor_{ℋ} A \in C_{ℋ} \land B \in C_{ℋ}) \to (x \lor_{ℋ} A) \cap B \in C_{ℋ}$
16	2 15	mpan2	$⊢ x \lor_{ℋ} A \in C_{ℋ} \to (x \lor_{ℋ} A) \cap B \in C_{ℋ}$
17	14 16	syl	$⊢ x \in C_{ℋ} \to (x \lor_{ℋ} A) \cap B \in C_{ℋ}$
18	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
19		chlub	$⊢ (x \in C_{ℋ} \land A \cap B \in C_{ℋ} \land (x \lor_{ℋ} A) \cap B \in C_{ℋ}) \to ((x \subseteq (x \lor_{ℋ} A) \cap B \land A \cap B \subseteq (x \lor_{ℋ} A) \cap B) \leftrightarrow x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B)$
20	18 19	mp3an2	$⊢ (x \in C_{ℋ} \land (x \lor_{ℋ} A) \cap B \in C_{ℋ}) \to ((x \subseteq (x \lor_{ℋ} A) \cap B \land A \cap B \subseteq (x \lor_{ℋ} A) \cap B) \leftrightarrow x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B)$
21	17 20	mpdan	$⊢ x \in C_{ℋ} \to ((x \subseteq (x \lor_{ℋ} A) \cap B \land A \cap B \subseteq (x \lor_{ℋ} A) \cap B) \leftrightarrow x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B)$
22	12 21	sylibd	$⊢ x \in C_{ℋ} \to (x \subseteq B \to x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B)$
23		eqss	$⊢ (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B) \leftrightarrow ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \land x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B)$
24	23	rbaib	$⊢ x \lor_{ℋ} (A \cap B) \subseteq (x \lor_{ℋ} A) \cap B \to ((x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B) \leftrightarrow (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B))$
25	22 24	syl6	$⊢ x \in C_{ℋ} \to (x \subseteq B \to ((x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B) \leftrightarrow (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
26	25	adantld	$⊢ x \in C_{ℋ} \to ((A \cap B \subseteq x \land x \subseteq B) \to ((x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B) \leftrightarrow (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
27	26	pm5.74d	$⊢ x \in C_{ℋ} \to (((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \leftrightarrow ((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
28	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
29		sstr	$⊢ (x \subseteq B \land B \subseteq A \lor_{ℋ} B) \to x \subseteq A \lor_{ℋ} B$
30	28 29	mpan2	$⊢ x \subseteq B \to x \subseteq A \lor_{ℋ} B$
31	30	pm4.71ri	$⊢ x \subseteq B \leftrightarrow (x \subseteq A \lor_{ℋ} B \land x \subseteq B)$
32	31	anbi2i	$⊢ (A \cap B \subseteq x \land x \subseteq B) \leftrightarrow (A \cap B \subseteq x \land (x \subseteq A \lor_{ℋ} B \land x \subseteq B))$
33		anass	$⊢ ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \land x \subseteq B) \leftrightarrow (A \cap B \subseteq x \land (x \subseteq A \lor_{ℋ} B \land x \subseteq B))$
34	32 33	bitr4i	$⊢ (A \cap B \subseteq x \land x \subseteq B) \leftrightarrow ((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \land x \subseteq B)$
35	34	imbi1i	$⊢ ((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \leftrightarrow (((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B))$
36	27 35	bitr3di	$⊢ x \in C_{ℋ} \to (((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)) \leftrightarrow (((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)))$
37		impexp	$⊢ (((A \cap B \subseteq x \land x \subseteq A \lor_{ℋ} B) \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)) \leftrightarrow ((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)))$
38	36 37	syl6bb	$⊢ x \in C_{ℋ} \to (((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)) \leftrightarrow ((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))))$
39	38	ralbiia	$⊢ \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)) \leftrightarrow \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)))$
40	1 2	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$
41	39 40	bitr2i	$⊢ A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} ((A \cap B \subseteq x \land x \subseteq B) \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B))$

Metamath Proof Explorer

Theorem mdsl2i

Proof