Metamath Proof Explorer

Theorem dmdbr5ati

Description: Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
Assertion dmdbr5ati ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
2 sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
3 dmdi4 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
4 1 2 3 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 𝑀ℋ* 𝐵 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
5 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
6 4 5 syl11 ⊢ ( 𝐴 𝑀ℋ* 𝐵 → ( 𝑥 ∈ HAtoms → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
7 6 a1dd ⊢ ( 𝐴 𝑀ℋ* 𝐵 → ( 𝑥 ∈ HAtoms → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
8 7 ralrimiv ⊢ ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
9 chjcom ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐵 ) )
10 2 5 9 sylancr ⊢ ( 𝑥 ∈ HAtoms → ( 𝐵 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐵 ) )
11 10 ineq1d ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) )
12 1 2 chjcomi ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐴 )
13 12 ineq2i ⊢ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
14 11 13 eqtr4di ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
15 14 adantr ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
16 12 sseq2i ⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
17 16 notbii ⊢ ( ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ¬ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐴 ) )
18 2 1 atabs2i ⊢ ( 𝑥 ∈ HAtoms → ( ¬ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐴 ) → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐵 ) )
19 18 imp ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐴 ) ) → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐵 )
20 17 19 sylan2b ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐵 ∨ℋ 𝑥 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐵 )
21 15 20 eqtr3d ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐵 )
22 chjcl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐵 ) ∈ Cℋ )
23 5 2 22 sylancl ⊢ ( 𝑥 ∈ HAtoms → ( 𝑥 ∨ℋ 𝐵 ) ∈ Cℋ )
24 chincl ⊢ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∈ Cℋ )
25 23 1 24 sylancl ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∈ Cℋ )
26 chub2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∈ Cℋ ) → 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
27 2 25 26 sylancr ⊢ ( 𝑥 ∈ HAtoms → 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
28 27 adantr ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
29 21 28 eqsstrd ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
30 29 ex ⊢ ( 𝑥 ∈ HAtoms → ( ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
31 30 biantrud ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ∧ ( ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) ) )
32 pm4.83 ⊢ ( ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ∧ ( ¬ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) ↔ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
33 31 32 bitrdi ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
34 33 ralbiia ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
35 1 2 sumdmdlem2 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
36 34 35 sylbi ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
37 1 2 sumdmdi ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 𝑀ℋ* 𝐵 )
38 36 37 sylib ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → 𝐴 𝑀ℋ* 𝐵 )
39 8 38 impbii ⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
40 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
41 40 biantru ⊢ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
42 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
43 chlub ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
44 2 42 43 mp3an23 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
45 41 44 bitrid ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
46 ssid ⊢ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∨ℋ 𝐵 )
47 46 biantrur ⊢ ( ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
48 ssin ⊢ ( ( ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
49 47 48 bitri ⊢ ( ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
50 45 49 bitrdi ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
51 50 biimpa ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
52 inss1 ⊢ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐵 )
53 51 52 jctil ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
54 eqss ⊢ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝑥 ∨ℋ 𝐵 ) ↔ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
55 53 54 sylibr ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝑥 ∨ℋ 𝐵 ) )
56 55 sseq1d ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
57 2 22 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ 𝐵 ) ∈ Cℋ )
58 57 1 24 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∈ Cℋ )
59 2 58 26 sylancr ⊢ ( 𝑥 ∈ Cℋ → 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
60 59 biantrud ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
61 chjcl ⊢ ( ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∈ Cℋ )
62 58 2 61 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∈ Cℋ )
63 chlub ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
64 2 63 mp3an2 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∈ Cℋ ) → ( ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
65 62 64 mpdan ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝐵 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
66 60 65 bitrd ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
67 66 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( 𝑥 ∨ℋ 𝐵 ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
68 56 67 bitr4d ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
69 68 pm5.74da ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
70 5 69 syl ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
71 70 ralbiia ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
72 39 71 bitri ⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )