Step |
Hyp |
Ref |
Expression |
1 |
|
0nelxp |
|- -. (/) e. ( _V X. _V ) |
2 |
|
ssel |
|- ( dom F C_ ( _V X. _V ) -> ( (/) e. dom F -> (/) e. ( _V X. _V ) ) ) |
3 |
1 2
|
mtoi |
|- ( dom F C_ ( _V X. _V ) -> -. (/) e. dom F ) |
4 |
|
df-rel |
|- ( Rel dom F <-> dom F C_ ( _V X. _V ) ) |
5 |
|
reldmtpos |
|- ( Rel dom tpos F <-> -. (/) e. dom F ) |
6 |
3 4 5
|
3imtr4i |
|- ( Rel dom F -> Rel dom tpos F ) |
7 |
|
relcnv |
|- Rel `' dom F |
8 |
6 7
|
jctir |
|- ( Rel dom F -> ( Rel dom tpos F /\ Rel `' dom F ) ) |
9 |
|
vex |
|- z e. _V |
10 |
|
brtpos |
|- ( z e. _V -> ( <. x , y >. tpos F z <-> <. y , x >. F z ) ) |
11 |
9 10
|
mp1i |
|- ( Rel dom F -> ( <. x , y >. tpos F z <-> <. y , x >. F z ) ) |
12 |
11
|
exbidv |
|- ( Rel dom F -> ( E. z <. x , y >. tpos F z <-> E. z <. y , x >. F z ) ) |
13 |
|
opex |
|- <. x , y >. e. _V |
14 |
13
|
eldm |
|- ( <. x , y >. e. dom tpos F <-> E. z <. x , y >. tpos F z ) |
15 |
|
vex |
|- x e. _V |
16 |
|
vex |
|- y e. _V |
17 |
15 16
|
opelcnv |
|- ( <. x , y >. e. `' dom F <-> <. y , x >. e. dom F ) |
18 |
|
opex |
|- <. y , x >. e. _V |
19 |
18
|
eldm |
|- ( <. y , x >. e. dom F <-> E. z <. y , x >. F z ) |
20 |
17 19
|
bitri |
|- ( <. x , y >. e. `' dom F <-> E. z <. y , x >. F z ) |
21 |
12 14 20
|
3bitr4g |
|- ( Rel dom F -> ( <. x , y >. e. dom tpos F <-> <. x , y >. e. `' dom F ) ) |
22 |
21
|
eqrelrdv2 |
|- ( ( ( Rel dom tpos F /\ Rel `' dom F ) /\ Rel dom F ) -> dom tpos F = `' dom F ) |
23 |
8 22
|
mpancom |
|- ( Rel dom F -> dom tpos F = `' dom F ) |