Metamath Proof Explorer

Theorem 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 ⊢ 𝐴 ∈ Cℋ
mdsl.2 ⊢ 𝐵 ∈ Cℋ
Assertion mdsl1i ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ↔ 𝐴 𝑀ℋ 𝐵 )

Proof

Step Hyp Ref Expression
1 mdsl.1 ⊢ 𝐴 ∈ Cℋ
2 mdsl.2 ⊢ 𝐵 ∈ Cℋ
3 sseq2 ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
4 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
5 3 4 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
6 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
7 oveq1 ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ∨ℋ 𝐴 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
8 7 ineq1d ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) )
9 oveq1 ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
11 6 10 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
12 5 11 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
13 12 rspccv ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
14 impexp ⊢ ( ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
15 impexp ⊢ ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ↔ ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
16 14 15 bitr2i ⊢ ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) ↔ ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
17 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
18 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
19 chlub ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
20 18 2 19 mp3an23 ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
21 20 biimpd ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
22 17 21 mpan2i ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) )
23 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
24 sstr ⊢ ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
25 23 24 mpan2 ⊢ ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
26 22 25 syl6 ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
27 chub2 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
28 18 27 mpan ⊢ ( 𝑦 ∈ Cℋ → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
29 26 28 jctild ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
30 chjcl ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ) → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ )
31 18 30 mpan2 ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ )
32 29 31 jctild ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
33 32 22 jcad ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) ) )
34 chjass ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) = ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
35 18 1 34 mp3an23 ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) = ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
36 18 1 chjcomi ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) )
37 1 2 chabs1i ⊢ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐴
38 36 37 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐴
39 38 oveq2i ⊢ ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) = ( 𝑦 ∨ℋ 𝐴 )
40 35 39 eqtrdi ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) = ( 𝑦 ∨ℋ 𝐴 ) )
41 40 ineq1d ⊢ ( 𝑦 ∈ Cℋ → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
42 chjass ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
43 18 18 42 mp3an23 ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
44 18 chjidmi ⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 )
45 44 oveq2i ⊢ ( 𝑦 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) )
46 43 45 eqtrdi ⊢ ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
47 41 46 eqeq12d ⊢ ( 𝑦 ∈ Cℋ → ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
48 47 biimpd ⊢ ( 𝑦 ∈ Cℋ → ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
49 33 48 imim12d ⊢ ( 𝑦 ∈ Cℋ → ( ( ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
50 16 49 syl5bi ⊢ ( 𝑦 ∈ Cℋ → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 → ( ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) → ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
51 13 50 syl5com ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) → ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
52 51 ralrimiv ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) → ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
53 mdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
54 1 2 53 mp2an ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
55 52 54 sylibr ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) → 𝐴 𝑀ℋ 𝐵 )
56 mdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
57 1 2 56 mp2an ⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
58 ax-1 ⊢ ( ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
59 58 ralimi ⊢ ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
60 57 59 sylbi ⊢ ( 𝐴 𝑀ℋ 𝐵 → ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
61 55 60 impbii ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ↔ 𝐴 𝑀ℋ 𝐵 )