This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dftpos3

Description: Alternate definition of tpos when F has relational domain. Compare df-cnv . (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dftpos3 
|- ( Rel dom F -> tpos F = { <. <. x , y >. , z >. | <. y , x >. F z } )

Proof

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 imbitrdi 
 |-  ( 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 eqabdv 
 |-  ( 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 } )