Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
|- Rel `' dom F |
2 |
|
dmtpos |
|- ( Rel dom F -> dom tpos F = `' dom F ) |
3 |
2
|
releqd |
|- ( Rel dom F -> ( Rel dom tpos F <-> Rel `' dom F ) ) |
4 |
1 3
|
mpbiri |
|- ( Rel dom F -> Rel dom tpos F ) |
5 |
|
reltpos |
|- Rel tpos F |
6 |
4 5
|
jctil |
|- ( Rel dom F -> ( Rel tpos F /\ Rel dom tpos F ) ) |
7 |
|
relrelss |
|- ( ( Rel tpos F /\ Rel dom tpos F ) <-> tpos F C_ ( ( _V X. _V ) X. _V ) ) |
8 |
6 7
|
sylib |
|- ( Rel dom F -> tpos F C_ ( ( _V X. _V ) X. _V ) ) |
9 |
8
|
sseld |
|- ( Rel dom F -> ( w e. tpos F -> w e. ( ( _V X. _V ) X. _V ) ) ) |
10 |
|
elvvv |
|- ( w e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z w = <. <. x , y >. , z >. ) |
11 |
9 10
|
syl6ib |
|- ( Rel dom F -> ( w e. tpos F -> E. x E. y E. z w = <. <. x , y >. , z >. ) ) |
12 |
11
|
pm4.71rd |
|- ( Rel dom F -> ( w e. tpos F <-> ( E. x E. y E. z w = <. <. x , y >. , z >. /\ w e. tpos F ) ) ) |
13 |
|
19.41vvv |
|- ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ w e. tpos F ) <-> ( E. x E. y E. z w = <. <. x , y >. , z >. /\ w e. tpos F ) ) |
14 |
|
eleq1 |
|- ( w = <. <. x , y >. , z >. -> ( w e. tpos F <-> <. <. x , y >. , z >. e. tpos F ) ) |
15 |
|
df-br |
|- ( <. x , y >. tpos F z <-> <. <. x , y >. , z >. e. tpos F ) |
16 |
|
brtpos |
|- ( z e. _V -> ( <. x , y >. tpos F z <-> <. y , x >. F z ) ) |
17 |
16
|
elv |
|- ( <. x , y >. tpos F z <-> <. y , x >. F z ) |
18 |
15 17
|
bitr3i |
|- ( <. <. x , y >. , z >. e. tpos F <-> <. y , x >. F z ) |
19 |
14 18
|
bitrdi |
|- ( w = <. <. x , y >. , z >. -> ( w e. tpos F <-> <. y , x >. F z ) ) |
20 |
19
|
pm5.32i |
|- ( ( w = <. <. x , y >. , z >. /\ w e. tpos F ) <-> ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) ) |
21 |
20
|
3exbii |
|- ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ w e. tpos F ) <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) ) |
22 |
13 21
|
bitr3i |
|- ( ( E. x E. y E. z w = <. <. x , y >. , z >. /\ w e. tpos F ) <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) ) |
23 |
12 22
|
bitrdi |
|- ( Rel dom F -> ( w e. tpos F <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) ) ) |
24 |
23
|
abbi2dv |
|- ( Rel dom F -> tpos F = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) } ) |
25 |
|
df-oprab |
|- { <. <. x , y >. , z >. | <. y , x >. F z } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ <. y , x >. F z ) } |
26 |
24 25
|
eqtr4di |
|- ( Rel dom F -> tpos F = { <. <. x , y >. , z >. | <. y , x >. F z } ) |