Theorem relbrtpos

Description: The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015)

	Ref	Expression
Assertion	relbrtpos	$$⊢\mathrm{Rel}F\to \left(⟨A,B⟩tposFC\leftrightarrow ⟨B,A⟩FC\right)$$

Proof

Step	Hyp	Ref	Expression
1		reltpos	$$⊢\mathrm{Rel}tposF$$
2	1	a1i	$$⊢\mathrm{Rel}F\to \mathrm{Rel}tposF$$
3		brrelex2	$$⊢\left(\mathrm{Rel}tposF\wedge ⟨A,B⟩tposFC\right)\to C\in \mathrm{V}$$
4	2 3	sylan	$$⊢\left(\mathrm{Rel}F\wedge ⟨A,B⟩tposFC\right)\to C\in \mathrm{V}$$
5		brrelex2	$$⊢\left(\mathrm{Rel}F\wedge ⟨B,A⟩FC\right)\to C\in \mathrm{V}$$
6		brtpos	$$⊢C\in \mathrm{V}\to \left(⟨A,B⟩tposFC\leftrightarrow ⟨B,A⟩FC\right)$$
7	4 5 6	pm5.21nd	$$⊢\mathrm{Rel}F\to \left(⟨A,B⟩tposFC\leftrightarrow ⟨B,A⟩FC\right)$$