# 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 ) → ( 𝐴 𝑀* 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝑀 ( ⊥ ‘ 𝐵 ) ) )