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 )