Theorem tposoprab

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

	Ref	Expression
Hypothesis	tposoprab.1	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
Assertion	tposoprab	$$⊢tposF=\left\{⟨⟨y,x⟩,z⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		tposoprab.1	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
2	1	tposeqi	$$⊢tposF=tpos\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
3		reldmoprab	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
4		dftpos3	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to tpos\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨a,b⟩,c⟩|⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}$$
5	3 4	ax-mp	$$⊢tpos\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨a,b⟩,c⟩|⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}y⟨b,a⟩$$
7		nfoprab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yc$$
9	6 7 8	nfbr	$$⊢Ⅎy⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}x⟨b,a⟩$$
11		nfoprab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xc$$
13	10 11 12	nfbr	$$⊢Ⅎx⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c$$
14		nfv	$$⊢Ⅎa⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c$$
15		nfv	$$⊢Ⅎb⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c$$
16		opeq12	$$⊢\left(b=x\wedge a=y\right)\to ⟨b,a⟩=⟨x,y⟩$$
17	16	ancoms	$$⊢\left(a=y\wedge b=x\right)\to ⟨b,a⟩=⟨x,y⟩$$
18	17	breq1d	$$⊢\left(a=y\wedge b=x\right)\to \left(⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\leftrightarrow ⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right)$$
19	9 13 14 15 18	cbvoprab12	$$⊢\left\{⟨⟨a,b⟩,c⟩|⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}=\left\{⟨⟨y,x⟩,c⟩|⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}z⟨x,y⟩$$
21		nfoprab3	$$⊢\underset{\_}{Ⅎ}z\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}zc$$
23	20 21 22	nfbr	$$⊢Ⅎz⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c$$
24		nfv	$$⊢Ⅎc\phi$$
25		breq2	$$⊢c=z\to \left(⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\leftrightarrow ⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}z\right)$$
26		df-br	$$⊢⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}z\leftrightarrow ⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
27		oprabidw	$$⊢⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \phi$$
28	26 27	bitri	$$⊢⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}z\leftrightarrow \phi$$
29	25 28	bitrdi	$$⊢c=z\to \left(⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\leftrightarrow \phi \right)$$
30	23 24 29	cbvoprab3	$$⊢\left\{⟨⟨y,x⟩,c⟩|⟨x,y⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}=\left\{⟨⟨y,x⟩,z⟩|\phi \right\}$$
31	19 30	eqtri	$$⊢\left\{⟨⟨a,b⟩,c⟩|⟨b,a⟩\left\{⟨⟨x,y⟩,z⟩|\phi \right\}c\right\}=\left\{⟨⟨y,x⟩,z⟩|\phi \right\}$$
32	2 5 31	3eqtri	$$⊢tposF=\left\{⟨⟨y,x⟩,z⟩|\phi \right\}$$