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