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 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
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 𝐹 = { ⟨ ⟨ 𝑦 , 𝑥 ⟩ , 𝑧 ⟩ ∣ 𝜑 }