Theorem tposoprab

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

	Ref	Expression
Hypothesis	tposoprab.1	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
Assertion	tposoprab	⊢ tpos 𝐹 = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑧 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		tposoprab.1	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
2	1	tposeqi	⊢ tpos 𝐹 = tpos { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
3		reldmoprab	⊢ Rel dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
4		dftpos3	⊢ ( Rel dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → tpos { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 } )
5	3 4	ax-mp	⊢ tpos { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 }
6		nfcv	⊢ Ⅎ 𝑦 ⟨ 𝑏 , 𝑎 ⟩
7		nfoprab2	⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
8		nfcv	⊢ Ⅎ 𝑦 𝑐
9	6 7 8	nfbr	⊢ Ⅎ 𝑦 ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐
10		nfcv	⊢ Ⅎ 𝑥 ⟨ 𝑏 , 𝑎 ⟩
11		nfoprab1	⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
12		nfcv	⊢ Ⅎ 𝑥 𝑐
13	10 11 12	nfbr	⊢ Ⅎ 𝑥 ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐
14		nfv	⊢ Ⅎ 𝑎 ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐
15		nfv	⊢ Ⅎ 𝑏 ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐
16		opeq12	⊢ ( ( 𝑏 = 𝑥 ∧ 𝑎 = 𝑦 ) → ⟨ 𝑏 , 𝑎 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
17	16	ancoms	⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ⟨ 𝑏 , 𝑎 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
18	17	breq1d	⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 ↔ ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 ) )
19	9 13 14 15 18	cbvoprab12	⊢ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 } = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 }
20		nfcv	⊢ Ⅎ 𝑧 ⟨ 𝑥 , 𝑦 ⟩
21		nfoprab3	⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
22		nfcv	⊢ Ⅎ 𝑧 𝑐
23	20 21 22	nfbr	⊢ Ⅎ 𝑧 ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐
24		nfv	⊢ Ⅎ 𝑐 𝜑
25		breq2	⊢ ( 𝑐 = 𝑧 → ( ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 ↔ ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑧 ) )
26		df-br	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
27		oprabidw	⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )
28	26 27	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑧 ↔ 𝜑 )
29	25 28	bitrdi	⊢ ( 𝑐 = 𝑧 → ( ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 ↔ 𝜑 ) )
30	23 24 29	cbvoprab3	⊢ { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 } = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
31	19 30	eqtri	⊢ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ⟨ 𝑏 , 𝑎 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑐 } = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
32	2 5 31	3eqtri	⊢ tpos 𝐹 = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑧 ⟩ ∣ 𝜑 }