Step | Hyp | Ref
| Expression |
1 | | relcnv 4646 |
. . . . . . . . . 10
⊢ Rel ◡dom 𝐹 |
2 | | dmtpos 5812 |
. . . . . . . . . . 11
⊢ (Rel dom
𝐹 → dom tpos 𝐹 = ◡dom 𝐹) |
3 | 2 | releqd 4367 |
. . . . . . . . . 10
⊢ (Rel dom
𝐹 → (Rel dom tpos
𝐹 ↔ Rel ◡dom 𝐹)) |
4 | 1, 3 | mpbiri 157 |
. . . . . . . . 9
⊢ (Rel dom
𝐹 → Rel dom tpos 𝐹) |
5 | | reltpos 5806 |
. . . . . . . . 9
⊢ Rel tpos
𝐹 |
6 | 4, 5 | jctil 295 |
. . . . . . . 8
⊢ (Rel dom
𝐹 → (Rel tpos 𝐹 ∧ Rel dom tpos 𝐹)) |
7 | | relrelss 4787 |
. . . . . . . 8
⊢ ((Rel
tpos 𝐹 ∧ Rel dom tpos 𝐹) ↔ tpos 𝐹 ⊆ ((V × V) ×
V)) |
8 | 6, 7 | sylib 127 |
. . . . . . 7
⊢ (Rel dom
𝐹 → tpos 𝐹 ⊆ ((V × V) ×
V)) |
9 | 8 | sseld 2938 |
. . . . . 6
⊢ (Rel dom
𝐹 → (w ∈ tpos 𝐹 → w ∈ ((V × V)
× V))) |
10 | | elvvv 4346 |
. . . . . 6
⊢ (w ∈ ((V × V)
× V) ↔ ∃x∃y∃z w =
〈〈x, y〉, z〉) |
11 | 9, 10 | syl6ib 150 |
. . . . 5
⊢ (Rel dom
𝐹 → (w ∈ tpos 𝐹 → ∃x∃y∃z w = 〈〈x, y〉,
z〉)) |
12 | 11 | pm4.71rd 374 |
. . . 4
⊢ (Rel dom
𝐹 → (w ∈ tpos 𝐹 ↔ (∃x∃y∃z w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹))) |
13 | | 19.41vvv 1781 |
. . . . 5
⊢ (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹) ↔ (∃x∃y∃z w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹)) |
14 | | eleq1 2097 |
. . . . . . . 8
⊢ (w = 〈〈x, y〉,
z〉 → (w ∈ tpos 𝐹 ↔ 〈〈x, y〉,
z〉 ∈
tpos 𝐹)) |
15 | | df-br 3756 |
. . . . . . . . 9
⊢
(〈x, y〉tpos 𝐹z ↔
〈〈x, y〉, z〉
∈ tpos 𝐹) |
16 | | vex 2554 |
. . . . . . . . . 10
⊢ x ∈
V |
17 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
18 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
19 | | brtposg 5810 |
. . . . . . . . . 10
⊢
((x ∈ V ∧ y ∈ V ∧ z ∈ V) → (〈x, y〉tpos
𝐹z ↔ 〈y, x〉𝐹z)) |
20 | 16, 17, 18, 19 | mp3an 1231 |
. . . . . . . . 9
⊢
(〈x, y〉tpos 𝐹z ↔
〈y, x〉𝐹z) |
21 | 15, 20 | bitr3i 175 |
. . . . . . . 8
⊢
(〈〈x, y〉, z〉
∈ tpos 𝐹 ↔ 〈y, x〉𝐹z) |
22 | 14, 21 | syl6bb 185 |
. . . . . . 7
⊢ (w = 〈〈x, y〉,
z〉 → (w ∈ tpos 𝐹 ↔ 〈y, x〉𝐹z)) |
23 | 22 | pm5.32i 427 |
. . . . . 6
⊢
((w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹) ↔ (w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z)) |
24 | 23 | 3exbii 1495 |
. . . . 5
⊢ (∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹) ↔ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z)) |
25 | 13, 24 | bitr3i 175 |
. . . 4
⊢ ((∃x∃y∃z w = 〈〈x, y〉,
z〉 ∧
w ∈ tpos
𝐹) ↔ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z)) |
26 | 12, 25 | syl6bb 185 |
. . 3
⊢ (Rel dom
𝐹 → (w ∈ tpos 𝐹 ↔ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z))) |
27 | 26 | abbi2dv 2153 |
. 2
⊢ (Rel dom
𝐹 → tpos 𝐹 = {w ∣ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z)}) |
28 | | df-oprab 5459 |
. 2
⊢
{〈〈x, y〉, z〉
∣ 〈y, x〉𝐹z} =
{w ∣ ∃x∃y∃z(w = 〈〈x, y〉,
z〉 ∧
〈y, x〉𝐹z)} |
29 | 27, 28 | syl6eqr 2087 |
1
⊢ (Rel dom
𝐹 → tpos 𝐹 = {〈〈x, y〉,
z〉 ∣ 〈y, x〉𝐹z}) |