Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 𝑀ℋ 𝑥 ↔ 𝐴 𝑀ℋ 𝑦 ) ) |
2 |
1
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑦 ∈ Cℋ 𝐴 𝑀ℋ 𝑦 ) |
3 |
|
mdbr |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ) ) |
4 |
|
chjcom |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐴 ) ) |
5 |
4
|
ineq1d |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∩ 𝑦 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) ) |
6 |
|
incom |
⊢ ( ( 𝐴 ∨ℋ 𝑥 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) |
7 |
5 6
|
eqtr3di |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
8 |
7
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
9 |
|
chincl |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 ∩ 𝑦 ) ∈ Cℋ ) |
10 |
|
chjcom |
⊢ ( ( ( 𝐴 ∩ 𝑦 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) |
11 |
9 10
|
sylan |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) |
12 |
|
incom |
⊢ ( 𝐴 ∩ 𝑦 ) = ( 𝑦 ∩ 𝐴 ) |
13 |
12
|
oveq1i |
⊢ ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) |
14 |
11 13
|
eqtr3di |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) ) |
15 |
8 14
|
eqeq12d |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ↔ ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) ) ) |
16 |
|
eqcom |
⊢ ( ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) ↔ ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
17 |
15 16
|
bitrdi |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ↔ ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) |
18 |
17
|
imbi2d |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ↔ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
19 |
18
|
ralbidva |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
20 |
3 19
|
bitrd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
21 |
20
|
ralbidva |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
22 |
2 21
|
syl5bb |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
23 |
|
ralcom |
⊢ ( ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) |
24 |
22 23
|
bitrdi |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
25 |
|
dmdbr |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝑥 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
26 |
25
|
ralbidva |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) ) |
27 |
24 26
|
bitr4d |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) ) |