Metamath Proof Explorer


Theorem dmtpos

Description: The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dmtpos
|- ( Rel dom F -> dom tpos F = `' dom F )

Proof

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 )