Metamath Proof Explorer

Theorem mdsl2bi

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

Ref Expression
Hypotheses mdsl.1 ⊢ 𝐴 ∈ Cℋ
mdsl.2 ⊢ 𝐵 ∈ Cℋ
Assertion mdsl2bi ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 mdsl.1 ⊢ 𝐴 ∈ Cℋ
2 mdsl.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 mdsl2i ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
4 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
5 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
6 chlej2 ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
7 5 6 mpan2 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
8 4 1 7 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
9 8 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
10 simpr ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ 𝐵 )
11 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
12 10 11 jctir ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) )
13 chlub ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑥 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
14 4 2 13 mp3an23 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
15 14 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
16 12 15 mpbid ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 )
17 9 16 ssind ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
18 17 biantrud ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
19 eqss ⊢ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
20 18 19 bitr4di ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
21 20 ex ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
22 21 adantld ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
23 22 pm5.74d ⊢ ( 𝑥 ∈ Cℋ → ( ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
24 23 ralbiia ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
25 3 24 bitri ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )