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 }