Metamath Proof Explorer

Theorem dmdmd

Description: The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of MaedaMaeda p. 130. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdmd ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝑀ℋ ( ⊥ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) ↔ ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
2 oveq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) )
3 2 ineq1d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
4 oveq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) )
5 3 4 eqeq12d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ↔ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
6 1 5 imbi12d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
7 6 rspccv ⊢ ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) → ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
8 choccl ⊢ ( 𝑥 ∈ Cℋ → ( ⊥ ‘ 𝑥 ) ∈ Cℋ )
9 8 imim1i ⊢ ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( 𝑥 ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
10 9 com12 ⊢ ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
12 chsscon3 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
13 12 biimpd ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
14 13 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
15 fveq2 ⊢ ( ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
16 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
17 chjcl ⊢ ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ )
18 8 16 17 syl2an ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ )
19 chdmm3 ⊢ ( ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∨ℋ 𝐵 ) )
20 18 19 sylan ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∨ℋ 𝐵 ) )
21 chdmj4 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑥 ∩ 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) = ( 𝑥 ∩ 𝐴 ) )
23 22 oveq1d ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∨ℋ 𝐵 ) = ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
24 20 23 eqtrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
25 24 anasss ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
26 choccl ⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
27 chincl ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ )
28 16 26 27 syl2an ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ )
29 chdmj2 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∩ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
30 28 29 sylan2 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∩ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
31 chdmm4 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
32 31 adantl ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
33 32 ineq2d ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( 𝑥 ∩ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
34 30 33 eqtrd ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
35 25 34 eqeq12d ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
36 35 ancoms ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
37 15 36 syl5ib ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
38 14 37 imim12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
39 11 38 syld ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
40 39 ex ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
41 40 com23 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ( ⊥ ‘ 𝑥 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝑥 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( 𝑥 ∈ Cℋ → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
42 7 41 syl5 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) → ( 𝑥 ∈ Cℋ → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
43 42 ralrimdv ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) → ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
44 sseq2 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) ) )
45 ineq1 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 ∩ 𝐴 ) = ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) )
46 45 oveq1d ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
47 ineq1 ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
48 46 47 eqeq12d ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
49 44 48 imbi12d ⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
50 49 rspccv ⊢ ( ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
51 choccl ⊢ ( 𝑦 ∈ Cℋ → ( ⊥ ‘ 𝑦 ) ∈ Cℋ )
52 51 imim1i ⊢ ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝑦 ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
53 52 com12 ⊢ ( 𝑦 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
54 53 adantl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
55 chsscon2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) ↔ 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) ) )
56 55 biimprd ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) ) )
57 56 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) ) )
58 fveq2 ⊢ ( ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
59 chincl ⊢ ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∈ Cℋ )
60 51 59 sylan ⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∈ Cℋ )
61 chdmj1 ⊢ ( ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
62 60 61 sylan ⊢ ( ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
63 chdmm2 ⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ) = ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) )
64 63 adantr ⊢ ( ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ) = ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) )
65 64 ineq1d ⊢ ( ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
66 62 65 eqtrd ⊢ ( ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
67 66 anasss ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) )
68 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
69 chdmm2 ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝑦 ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
70 68 69 sylan2 ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝑦 ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
71 chdmj1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) )
72 71 adantl ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) )
73 72 oveq2d ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( 𝑦 ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) )
74 70 73 eqtrd ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) )
75 67 74 eqeq12d ⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) → ( ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
76 75 ancoms ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ⊥ ‘ ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
77 58 76 syl5ib ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
78 57 77 imim12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
79 54 78 syld ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
80 79 ex ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑦 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) ) )
81 80 com23 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ → ( 𝐵 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( ⊥ ‘ 𝑦 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ⊥ ‘ 𝑦 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) ) )
82 50 81 syl5 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) ) )
83 82 ralrimdv ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
84 43 83 impbid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
85 mdbr ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) 𝑀ℋ ( ⊥ ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
86 16 26 85 syl2an ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) 𝑀ℋ ( ⊥ ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝑦 ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑦 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ) )
87 dmdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
88 84 86 87 3bitr4rd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝑀ℋ ( ⊥ ‘ 𝐵 ) ) )