Step |
Hyp |
Ref |
Expression |
1 |
|
mdbr |
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) |
2 |
|
chub1 |
|- ( ( x e. CH /\ A e. CH ) -> x C_ ( x vH A ) ) |
3 |
2
|
ancoms |
|- ( ( A e. CH /\ x e. CH ) -> x C_ ( x vH A ) ) |
4 |
|
iba |
|- ( x C_ B -> ( x C_ ( x vH A ) <-> ( x C_ ( x vH A ) /\ x C_ B ) ) ) |
5 |
|
ssin |
|- ( ( x C_ ( x vH A ) /\ x C_ B ) <-> x C_ ( ( x vH A ) i^i B ) ) |
6 |
4 5
|
syl6bb |
|- ( x C_ B -> ( x C_ ( x vH A ) <-> x C_ ( ( x vH A ) i^i B ) ) ) |
7 |
3 6
|
syl5ibcom |
|- ( ( A e. CH /\ x e. CH ) -> ( x C_ B -> x C_ ( ( x vH A ) i^i B ) ) ) |
8 |
|
chub2 |
|- ( ( A e. CH /\ x e. CH ) -> A C_ ( x vH A ) ) |
9 |
8
|
ssrind |
|- ( ( A e. CH /\ x e. CH ) -> ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) |
10 |
7 9
|
jctird |
|- ( ( A e. CH /\ x e. CH ) -> ( x C_ B -> ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) ) ) |
11 |
10
|
adantlr |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) ) ) |
12 |
|
simpr |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> x e. CH ) |
13 |
|
chincl |
|- ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH ) |
14 |
13
|
adantr |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( A i^i B ) e. CH ) |
15 |
|
chjcl |
|- ( ( x e. CH /\ A e. CH ) -> ( x vH A ) e. CH ) |
16 |
15
|
ancoms |
|- ( ( A e. CH /\ x e. CH ) -> ( x vH A ) e. CH ) |
17 |
|
chincl |
|- ( ( ( x vH A ) e. CH /\ B e. CH ) -> ( ( x vH A ) i^i B ) e. CH ) |
18 |
16 17
|
sylan |
|- ( ( ( A e. CH /\ x e. CH ) /\ B e. CH ) -> ( ( x vH A ) i^i B ) e. CH ) |
19 |
18
|
an32s |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x vH A ) i^i B ) e. CH ) |
20 |
|
chlub |
|- ( ( x e. CH /\ ( A i^i B ) e. CH /\ ( ( x vH A ) i^i B ) e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) ) |
21 |
12 14 19 20
|
syl3anc |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) ) |
22 |
11 21
|
sylibd |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) ) |
23 |
|
eqss |
|- ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) /\ ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) ) |
24 |
23
|
rbaib |
|- ( ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) |
25 |
22 24
|
syl6 |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) ) |
26 |
25
|
pm5.74d |
|- ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) ) |
27 |
26
|
ralbidva |
|- ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) ) |
28 |
1 27
|
bitrd |
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) ) |