Step |
Hyp |
Ref |
Expression |
1 |
|
cmtfval.b |
|- B = ( Base ` K ) |
2 |
|
cmtfval.j |
|- .\/ = ( join ` K ) |
3 |
|
cmtfval.m |
|- ./\ = ( meet ` K ) |
4 |
|
cmtfval.o |
|- ._|_ = ( oc ` K ) |
5 |
|
cmtfval.c |
|- C = ( cm ` K ) |
6 |
1 2 3 4 5
|
cmtfvalN |
|- ( K e. A -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } ) |
7 |
|
df-3an |
|- ( ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) <-> ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) ) |
8 |
7
|
opabbii |
|- { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } |
9 |
6 8
|
eqtrdi |
|- ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } ) |
10 |
9
|
breqd |
|- ( K e. A -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y ) ) |
11 |
10
|
3ad2ant1 |
|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y ) ) |
12 |
|
df-br |
|- ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } ) |
13 |
|
id |
|- ( x = X -> x = X ) |
14 |
|
oveq1 |
|- ( x = X -> ( x ./\ y ) = ( X ./\ y ) ) |
15 |
|
oveq1 |
|- ( x = X -> ( x ./\ ( ._|_ ` y ) ) = ( X ./\ ( ._|_ ` y ) ) ) |
16 |
14 15
|
oveq12d |
|- ( x = X -> ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) ) |
17 |
13 16
|
eqeq12d |
|- ( x = X -> ( x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) <-> X = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) ) ) |
18 |
|
oveq2 |
|- ( y = Y -> ( X ./\ y ) = ( X ./\ Y ) ) |
19 |
|
fveq2 |
|- ( y = Y -> ( ._|_ ` y ) = ( ._|_ ` Y ) ) |
20 |
19
|
oveq2d |
|- ( y = Y -> ( X ./\ ( ._|_ ` y ) ) = ( X ./\ ( ._|_ ` Y ) ) ) |
21 |
18 20
|
oveq12d |
|- ( y = Y -> ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) |
22 |
21
|
eqeq2d |
|- ( y = Y -> ( X = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) ) |
23 |
17 22
|
opelopab2 |
|- ( ( X e. B /\ Y e. B ) -> ( <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) ) |
24 |
12 23
|
syl5bb |
|- ( ( X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) ) |
25 |
24
|
3adant1 |
|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) ) |
26 |
11 25
|
bitrd |
|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) ) |