This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmdbr5

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005) (New usage is discouraged.)

Ref Expression
Assertion dmdbr5 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 dmdbr4 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
2 chub1 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐵 ) )
3 2 ancoms ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐵 ) )
4 ssin ⊢ ( ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
5 sstr2 ⊢ ( 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
6 4 5 sylbi ⊢ ( ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
7 3 6 sylan ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
8 7 ex ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
9 8 com23 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
10 9 ralimdva ⊢ ( 𝐵 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
12 1 11 sylbid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
13 sseq1 ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
14 id ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
15 oveq1 ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ∨ℋ 𝐵 ) = ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) )
16 15 ineq1d ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) )
17 16 oveq1d ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
18 14 17 sseq12d ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
19 13 18 imbi12d ⊢ ( 𝑥 = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
20 19 rspccv ⊢ ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
21 chjcl ⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑦 ∨ℋ 𝐵 ) ∈ Cℋ )
22 21 ancoms ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ∨ℋ 𝐵 ) ∈ Cℋ )
23 22 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ∨ℋ 𝐵 ) ∈ Cℋ )
24 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
25 24 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
26 chincl ⊢ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ )
27 23 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ )
28 inss2 ⊢ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
29 pm2.27 ⊢ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
30 28 29 mpii ⊢ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
31 27 30 syl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
32 chub2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → 𝐵 ⊆ ( 𝑦 ∨ℋ 𝐵 ) )
33 32 adantll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → 𝐵 ⊆ ( 𝑦 ∨ℋ 𝐵 ) )
34 chub2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
35 34 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
37 33 36 ssind ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → 𝐵 ⊆ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
38 simplr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → 𝐵 ∈ Cℋ )
39 chlejb2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ ) → ( 𝐵 ⊆ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
40 38 27 39 syl2anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝐵 ⊆ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
41 37 40 mpbid ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
42 41 ineq1d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐴 ) )
43 inass ⊢ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
44 incom ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
45 chabs2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 )
46 44 45 eqtrid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐴 ) = 𝐴 )
47 46 ineq2d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐴 ) ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
48 43 47 eqtrid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
49 48 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
50 42 49 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
51 50 oveq1d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
52 51 sseq2d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
53 31 52 sylibd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
54 53 ex ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑦 ∈ Cℋ → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
55 54 com23 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ → ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) → ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
56 20 55 syl5 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → ( 𝑦 ∈ Cℋ → ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
57 56 ralrimdv ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → ∀ 𝑦 ∈ Cℋ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
58 dmdbr4 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑦 ∈ Cℋ ( ( 𝑦 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑦 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
59 57 58 sylibrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → 𝐴 𝑀ℋ* 𝐵 ) )
60 12 59 impbid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )