Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
|- ( x = y -> ( A MH x <-> A MH y ) ) |
2 |
1
|
cbvralvw |
|- ( A. x e. CH A MH x <-> A. y e. CH A MH y ) |
3 |
|
mdbr |
|- ( ( A e. CH /\ y e. CH ) -> ( A MH y <-> A. x e. CH ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) ) ) |
4 |
|
incom |
|- ( ( A vH x ) i^i y ) = ( y i^i ( A vH x ) ) |
5 |
|
chjcom |
|- ( ( A e. CH /\ x e. CH ) -> ( A vH x ) = ( x vH A ) ) |
6 |
5
|
ineq1d |
|- ( ( A e. CH /\ x e. CH ) -> ( ( A vH x ) i^i y ) = ( ( x vH A ) i^i y ) ) |
7 |
4 6
|
syl5reqr |
|- ( ( A e. CH /\ x e. CH ) -> ( ( x vH A ) i^i y ) = ( y i^i ( A vH x ) ) ) |
8 |
7
|
adantlr |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( x vH A ) i^i y ) = ( y i^i ( A vH x ) ) ) |
9 |
|
incom |
|- ( A i^i y ) = ( y i^i A ) |
10 |
9
|
oveq1i |
|- ( ( A i^i y ) vH x ) = ( ( y i^i A ) vH x ) |
11 |
|
chincl |
|- ( ( A e. CH /\ y e. CH ) -> ( A i^i y ) e. CH ) |
12 |
|
chjcom |
|- ( ( ( A i^i y ) e. CH /\ x e. CH ) -> ( ( A i^i y ) vH x ) = ( x vH ( A i^i y ) ) ) |
13 |
11 12
|
sylan |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( A i^i y ) vH x ) = ( x vH ( A i^i y ) ) ) |
14 |
10 13
|
syl5reqr |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( x vH ( A i^i y ) ) = ( ( y i^i A ) vH x ) ) |
15 |
8 14
|
eqeq12d |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) <-> ( y i^i ( A vH x ) ) = ( ( y i^i A ) vH x ) ) ) |
16 |
|
eqcom |
|- ( ( y i^i ( A vH x ) ) = ( ( y i^i A ) vH x ) <-> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) |
17 |
15 16
|
syl6bb |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) <-> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) |
18 |
17
|
imbi2d |
|- ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) <-> ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
19 |
18
|
ralbidva |
|- ( ( A e. CH /\ y e. CH ) -> ( A. x e. CH ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) <-> A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
20 |
3 19
|
bitrd |
|- ( ( A e. CH /\ y e. CH ) -> ( A MH y <-> A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
21 |
20
|
ralbidva |
|- ( A e. CH -> ( A. y e. CH A MH y <-> A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
22 |
2 21
|
syl5bb |
|- ( A e. CH -> ( A. x e. CH A MH x <-> A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
23 |
|
ralcom |
|- ( A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) |
24 |
22 23
|
syl6bb |
|- ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
25 |
|
dmdbr |
|- ( ( A e. CH /\ x e. CH ) -> ( A MH* x <-> A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
26 |
25
|
ralbidva |
|- ( A e. CH -> ( A. x e. CH A MH* x <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) ) |
27 |
24 26
|
bitr4d |
|- ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A MH* x ) ) |