Step | Hyp | Ref
| Expression |
1 | | relcnv 4989 |
. . . . . . . . . 10
⊢ Rel ◡dom 𝐹 |
2 | | dmtpos 6235 |
. . . . . . . . . . 11
⊢ (Rel dom
𝐹 → dom tpos 𝐹 = ◡dom 𝐹) |
3 | 2 | releqd 4695 |
. . . . . . . . . 10
⊢ (Rel dom
𝐹 → (Rel dom tpos
𝐹 ↔ Rel ◡dom 𝐹)) |
4 | 1, 3 | mpbiri 167 |
. . . . . . . . 9
⊢ (Rel dom
𝐹 → Rel dom tpos 𝐹) |
5 | | reltpos 6229 |
. . . . . . . . 9
⊢ Rel tpos
𝐹 |
6 | 4, 5 | jctil 310 |
. . . . . . . 8
⊢ (Rel dom
𝐹 → (Rel tpos 𝐹 ∧ Rel dom tpos 𝐹)) |
7 | | relrelss 5137 |
. . . . . . . 8
⊢ ((Rel
tpos 𝐹 ∧ Rel dom tpos
𝐹) ↔ tpos 𝐹 ⊆ ((V × V) ×
V)) |
8 | 6, 7 | sylib 121 |
. . . . . . 7
⊢ (Rel dom
𝐹 → tpos 𝐹 ⊆ ((V × V) ×
V)) |
9 | 8 | sseld 3146 |
. . . . . 6
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 → 𝑤 ∈ ((V × V) ×
V))) |
10 | | elvvv 4674 |
. . . . . 6
⊢ (𝑤 ∈ ((V × V) ×
V) ↔ ∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
11 | 9, 10 | syl6ib 160 |
. . . . 5
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 → ∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
12 | 11 | pm4.71rd 392 |
. . . 4
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 ↔ (∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹))) |
13 | | 19.41vvv 1897 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ (∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹)) |
14 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑤 ∈ tpos 𝐹 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ tpos 𝐹)) |
15 | | df-br 3990 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ tpos 𝐹) |
16 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
17 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
18 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
19 | | brtposg 6233 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉𝐹𝑧)) |
20 | 16, 17, 18, 19 | mp3an 1332 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉𝐹𝑧) |
21 | 15, 20 | bitr3i 185 |
. . . . . . . 8
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ tpos 𝐹 ↔ 〈𝑦, 𝑥〉𝐹𝑧) |
22 | 14, 21 | bitrdi 195 |
. . . . . . 7
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑤 ∈ tpos 𝐹 ↔ 〈𝑦, 𝑥〉𝐹𝑧)) |
23 | 22 | pm5.32i 451 |
. . . . . 6
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) |
24 | 23 | 3exbii 1600 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) |
25 | 13, 24 | bitr3i 185 |
. . . 4
⊢
((∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) |
26 | 12, 25 | bitrdi 195 |
. . 3
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧))) |
27 | 26 | abbi2dv 2289 |
. 2
⊢ (Rel dom
𝐹 → tpos 𝐹 = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)}) |
28 | | df-oprab 5857 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)} |
29 | 27, 28 | eqtr4di 2221 |
1
⊢ (Rel dom
𝐹 → tpos 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧}) |