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