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

Metamath Proof Explorer

Theorem tposoprab

Description: Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis tposoprab.1 
|- F = { <. <. x , y >. , z >. | ph }
Assertion tposoprab 
|- tpos F = { <. <. y , x >. , z >. | ph }

Proof

Step Hyp Ref Expression
1 tposoprab.1 
 |-  F = { <. <. x , y >. , z >. | ph }
2 1 tposeqi 
 |-  tpos F = tpos { <. <. x , y >. , z >. | ph }
3 reldmoprab 
 |-  Rel dom { <. <. x , y >. , z >. | ph }
4 dftpos3 
 |-  ( Rel dom { <. <. x , y >. , z >. | ph } -> tpos { <. <. x , y >. , z >. | ph } = { <. <. a , b >. , c >. | <. b , a >. { <. <. x , y >. , z >. | ph } c } )
5 3 4 ax-mp 
 |-  tpos { <. <. x , y >. , z >. | ph } = { <. <. a , b >. , c >. | <. b , a >. { <. <. x , y >. , z >. | ph } c }
6 nfcv 
 |-  F/_ y <. b , a >.
7 nfoprab2 
 |-  F/_ y { <. <. x , y >. , z >. | ph }
8 nfcv 
 |-  F/_ y c
9 6 7 8 nfbr 
 |-  F/ y <. b , a >. { <. <. x , y >. , z >. | ph } c
10 nfcv 
 |-  F/_ x <. b , a >.
11 nfoprab1 
 |-  F/_ x { <. <. x , y >. , z >. | ph }
12 nfcv 
 |-  F/_ x c
13 10 11 12 nfbr 
 |-  F/ x <. b , a >. { <. <. x , y >. , z >. | ph } c
14 nfv 
 |-  F/ a <. x , y >. { <. <. x , y >. , z >. | ph } c
15 nfv 
 |-  F/ b <. x , y >. { <. <. x , y >. , z >. | ph } c
16 opeq12 
 |-  ( ( b = x /\ a = y ) -> <. b , a >. = <. x , y >. )
17 16 ancoms 
 |-  ( ( a = y /\ b = x ) -> <. b , a >. = <. x , y >. )
18 17 breq1d 
 |-  ( ( a = y /\ b = x ) -> ( <. b , a >. { <. <. x , y >. , z >. | ph } c <-> <. x , y >. { <. <. x , y >. , z >. | ph } c ) )
19 9 13 14 15 18 cbvoprab12 
 |-  { <. <. a , b >. , c >. | <. b , a >. { <. <. x , y >. , z >. | ph } c } = { <. <. y , x >. , c >. | <. x , y >. { <. <. x , y >. , z >. | ph } c }
20 nfcv 
 |-  F/_ z <. x , y >.
21 nfoprab3 
 |-  F/_ z { <. <. x , y >. , z >. | ph }
22 nfcv 
 |-  F/_ z c
23 20 21 22 nfbr 
 |-  F/ z <. x , y >. { <. <. x , y >. , z >. | ph } c
24 nfv 
 |-  F/ c ph
25 breq2 
 |-  ( c = z -> ( <. x , y >. { <. <. x , y >. , z >. | ph } c <-> <. x , y >. { <. <. x , y >. , z >. | ph } z ) )
26 df-br 
 |-  ( <. x , y >. { <. <. x , y >. , z >. | ph } z <-> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } )
27 oprabidw 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
28 26 27 bitri 
 |-  ( <. x , y >. { <. <. x , y >. , z >. | ph } z <-> ph )
29 25 28 bitrdi 
 |-  ( c = z -> ( <. x , y >. { <. <. x , y >. , z >. | ph } c <-> ph ) )
30 23 24 29 cbvoprab3 
 |-  { <. <. y , x >. , c >. | <. x , y >. { <. <. x , y >. , z >. | ph } c } = { <. <. y , x >. , z >. | ph }
31 19 30 eqtri 
 |-  { <. <. a , b >. , c >. | <. b , a >. { <. <. x , y >. , z >. | ph } c } = { <. <. y , x >. , z >. | ph }
32 2 5 31 3eqtri 
 |-  tpos F = { <. <. y , x >. , z >. | ph }