| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relcnv 6122 | . . . . . . . . . 10
⊢ Rel ◡dom 𝐹 | 
| 2 |  | dmtpos 8263 | . . . . . . . . . . 11
⊢ (Rel dom
𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | 
| 3 | 2 | releqd 5788 | . . . . . . . . . 10
⊢ (Rel dom
𝐹 → (Rel dom tpos
𝐹 ↔ Rel ◡dom 𝐹)) | 
| 4 | 1, 3 | mpbiri 258 | . . . . . . . . 9
⊢ (Rel dom
𝐹 → Rel dom tpos 𝐹) | 
| 5 |  | reltpos 8256 | . . . . . . . . 9
⊢ Rel tpos
𝐹 | 
| 6 | 4, 5 | jctil 519 | . . . . . . . 8
⊢ (Rel dom
𝐹 → (Rel tpos 𝐹 ∧ Rel dom tpos 𝐹)) | 
| 7 |  | relrelss 6293 | . . . . . . . 8
⊢ ((Rel
tpos 𝐹 ∧ Rel dom tpos
𝐹) ↔ tpos 𝐹 ⊆ ((V × V) ×
V)) | 
| 8 | 6, 7 | sylib 218 | . . . . . . 7
⊢ (Rel dom
𝐹 → tpos 𝐹 ⊆ ((V × V) ×
V)) | 
| 9 | 8 | sseld 3982 | . . . . . 6
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 → 𝑤 ∈ ((V × V) ×
V))) | 
| 10 |  | elvvv 5761 | . . . . . 6
⊢ (𝑤 ∈ ((V × V) ×
V) ↔ ∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉) | 
| 11 | 9, 10 | imbitrdi 251 | . . . . 5
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 → ∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉)) | 
| 12 | 11 | pm4.71rd 562 | . . . 4
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 ↔ (∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹))) | 
| 13 |  | 19.41vvv 1951 | . . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ (∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹)) | 
| 14 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑤 ∈ tpos 𝐹 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ tpos 𝐹)) | 
| 15 |  | df-br 5144 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ tpos 𝐹) | 
| 16 |  | brtpos 8260 | . . . . . . . . . 10
⊢ (𝑧 ∈ V → (〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉𝐹𝑧)) | 
| 17 | 16 | elv 3485 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉𝐹𝑧) | 
| 18 | 15, 17 | bitr3i 277 | . . . . . . . 8
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ tpos 𝐹 ↔ 〈𝑦, 𝑥〉𝐹𝑧) | 
| 19 | 14, 18 | bitrdi 287 | . . . . . . 7
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑤 ∈ tpos 𝐹 ↔ 〈𝑦, 𝑥〉𝐹𝑧)) | 
| 20 | 19 | pm5.32i 574 | . . . . . 6
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) | 
| 21 | 20 | 3exbii 1850 | . . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) | 
| 22 | 13, 21 | bitr3i 277 | . . . 4
⊢
((∃𝑥∃𝑦∃𝑧 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 ∈ tpos 𝐹) ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)) | 
| 23 | 12, 22 | bitrdi 287 | . . 3
⊢ (Rel dom
𝐹 → (𝑤 ∈ tpos 𝐹 ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧))) | 
| 24 | 23 | eqabdv 2875 | . 2
⊢ (Rel dom
𝐹 → tpos 𝐹 = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)}) | 
| 25 |  | df-oprab 7435 | . 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 〈𝑦, 𝑥〉𝐹𝑧)} | 
| 26 | 24, 25 | eqtr4di 2795 | 1
⊢ (Rel dom
𝐹 → tpos 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧}) |