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 }