Step |
Hyp |
Ref |
Expression |
1 |
|
brinxp |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A A ( |
2 |
|
df-ltnq |
|- |
3 |
2
|
breqi |
|- ( A A ( |
4 |
1 3
|
bitr4di |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A A |
5 |
|
relxp |
|- Rel ( N. X. N. ) |
6 |
|
elpqn |
|- ( A e. Q. -> A e. ( N. X. N. ) ) |
7 |
|
1st2nd |
|- ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
8 |
5 6 7
|
sylancr |
|- ( A e. Q. -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
9 |
|
elpqn |
|- ( B e. Q. -> B e. ( N. X. N. ) ) |
10 |
|
1st2nd |
|- ( ( Rel ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. ) |
11 |
5 9 10
|
sylancr |
|- ( B e. Q. -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. ) |
12 |
8 11
|
breqan12d |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <. ( 1st ` A ) , ( 2nd ` A ) >. . ) ) |
13 |
|
ordpipq |
|- ( <. ( 1st ` A ) , ( 2nd ` A ) >. . <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) |
14 |
12 13
|
bitrdi |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A ( ( 1st ` A ) .N ( 2nd ` B ) ) |
15 |
4 14
|
bitr3d |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A ( ( 1st ` A ) .N ( 2nd ` B ) ) |