Step | Hyp | Ref
| Expression |
1 | | tposoprab.1 |
. . 3
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
2 | 1 | tposeqi 6256 |
. 2
⊢ tpos
𝐹 = tpos {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
3 | | reldmoprab 5938 |
. . 3
⊢ Rel dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
4 | | dftpos3 6241 |
. . 3
⊢ (Rel dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} → tpos {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ 〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐}) |
5 | 3, 4 | ax-mp 5 |
. 2
⊢ tpos
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ 〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐} |
6 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑦〈𝑏, 𝑎〉 |
7 | | nfoprab2 5903 |
. . . . 5
⊢
Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
8 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑦𝑐 |
9 | 6, 7, 8 | nfbr 4035 |
. . . 4
⊢
Ⅎ𝑦〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 |
10 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑥〈𝑏, 𝑎〉 |
11 | | nfoprab1 5902 |
. . . . 5
⊢
Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
12 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑥𝑐 |
13 | 10, 11, 12 | nfbr 4035 |
. . . 4
⊢
Ⅎ𝑥〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 |
14 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑎〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 |
15 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑏〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 |
16 | | opeq12 3767 |
. . . . . 6
⊢ ((𝑏 = 𝑥 ∧ 𝑎 = 𝑦) → 〈𝑏, 𝑎〉 = 〈𝑥, 𝑦〉) |
17 | 16 | ancoms 266 |
. . . . 5
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → 〈𝑏, 𝑎〉 = 〈𝑥, 𝑦〉) |
18 | 17 | breq1d 3999 |
. . . 4
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 ↔ 〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐)) |
19 | 9, 13, 14, 15, 18 | cbvoprab12 5927 |
. . 3
⊢
{〈〈𝑎,
𝑏〉, 𝑐〉 ∣ 〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐} = {〈〈𝑦, 𝑥〉, 𝑐〉 ∣ 〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐} |
20 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑧〈𝑥, 𝑦〉 |
21 | | nfoprab3 5904 |
. . . . 5
⊢
Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
22 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑧𝑐 |
23 | 20, 21, 22 | nfbr 4035 |
. . . 4
⊢
Ⅎ𝑧〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 |
24 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑐𝜑 |
25 | | breq2 3993 |
. . . . 5
⊢ (𝑐 = 𝑧 → (〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 ↔ 〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑧)) |
26 | | df-br 3990 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑧 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
27 | | oprabid 5885 |
. . . . . 6
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |
28 | 26, 27 | bitri 183 |
. . . . 5
⊢
(〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑧 ↔ 𝜑) |
29 | 25, 28 | bitrdi 195 |
. . . 4
⊢ (𝑐 = 𝑧 → (〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐 ↔ 𝜑)) |
30 | 23, 24, 29 | cbvoprab3 5929 |
. . 3
⊢
{〈〈𝑦,
𝑥〉, 𝑐〉 ∣ 〈𝑥, 𝑦〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐} = {〈〈𝑦, 𝑥〉, 𝑧〉 ∣ 𝜑} |
31 | 19, 30 | eqtri 2191 |
. 2
⊢
{〈〈𝑎,
𝑏〉, 𝑐〉 ∣ 〈𝑏, 𝑎〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑐} = {〈〈𝑦, 𝑥〉, 𝑧〉 ∣ 𝜑} |
32 | 2, 5, 31 | 3eqtri 2195 |
1
⊢ tpos
𝐹 = {〈〈𝑦, 𝑥〉, 𝑧〉 ∣ 𝜑} |