Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
|- ( a = A -> ( a e. X <-> A e. X ) ) |
2 |
|
eleq1 |
|- ( b = B -> ( b e. X <-> B e. X ) ) |
3 |
1 2
|
bi2anan9 |
|- ( ( a = A /\ b = B ) -> ( ( a e. X /\ b e. X ) <-> ( A e. X /\ B e. X ) ) ) |
4 |
|
oveq12 |
|- ( ( a = A /\ b = B ) -> ( a D b ) = ( A D B ) ) |
5 |
4
|
eqeq1d |
|- ( ( a = A /\ b = B ) -> ( ( a D b ) = 0 <-> ( A D B ) = 0 ) ) |
6 |
3 5
|
anbi12d |
|- ( ( a = A /\ b = B ) -> ( ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) ) |
7 |
|
eqid |
|- { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } |
8 |
6 7
|
brabga |
|- ( ( A e. X /\ B e. X ) -> ( A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) ) |
9 |
8
|
adantl |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) ) |
10 |
|
metidval |
|- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } ) |
11 |
10
|
adantr |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( ~Met ` D ) = { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } ) |
12 |
11
|
breqd |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A ( ~Met ` D ) B <-> A { <. a , b >. | ( ( a e. X /\ b e. X ) /\ ( a D b ) = 0 ) } B ) ) |
13 |
|
ibar |
|- ( ( A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) ) |
14 |
13
|
adantl |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) = 0 <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) = 0 ) ) ) |
15 |
9 12 14
|
3bitr4d |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A ( ~Met ` D ) B <-> ( A D B ) = 0 ) ) |