| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reltpos 8257 | . 2
⊢ Rel tpos
tpos 𝐹 | 
| 2 |  | relinxp 5823 | . 2
⊢ Rel
(𝐹 ∩ (((V × V)
∪ {∅}) × V)) | 
| 3 |  | relcnv 6121 | . . . . . . . . 9
⊢ Rel ◡dom tpos 𝐹 | 
| 4 |  | df-rel 5691 | . . . . . . . . 9
⊢ (Rel
◡dom tpos 𝐹 ↔ ◡dom tpos 𝐹 ⊆ (V × V)) | 
| 5 | 3, 4 | mpbi 230 | . . . . . . . 8
⊢ ◡dom tpos 𝐹 ⊆ (V × V) | 
| 6 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ ◡dom tpos 𝐹) | 
| 7 | 5, 6 | sselid 3980 | . . . . . . 7
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ (V × V)) | 
| 8 |  | simpr 484 | . . . . . . 7
⊢ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) → 𝑤 ∈ (V ×
V)) | 
| 9 |  | elvv 5759 | . . . . . . . . 9
⊢ (𝑤 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉) | 
| 10 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ ◡dom tpos 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ ◡dom tpos 𝐹)) | 
| 11 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V | 
| 12 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V | 
| 13 | 11, 12 | opelcnv 5891 | . . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ◡dom tpos 𝐹 ↔ 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹) | 
| 14 | 10, 13 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ ◡dom tpos 𝐹 ↔ 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹)) | 
| 15 |  | sneq 4635 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑥, 𝑦〉 → {𝑤} = {〈𝑥, 𝑦〉}) | 
| 16 | 15 | cnveqd 5885 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ◡{𝑤} = ◡{〈𝑥, 𝑦〉}) | 
| 17 | 16 | unieqd 4919 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ∪
◡{𝑤} = ∪ ◡{〈𝑥, 𝑦〉}) | 
| 18 |  | opswap 6248 | . . . . . . . . . . . . . . 15
⊢ ∪ ◡{〈𝑥, 𝑦〉} = 〈𝑦, 𝑥〉 | 
| 19 | 17, 18 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ∪
◡{𝑤} = 〈𝑦, 𝑥〉) | 
| 20 | 19 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (∪
◡{𝑤}tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉tpos 𝐹𝑧)) | 
| 21 | 14, 20 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧))) | 
| 22 |  | opex 5468 | . . . . . . . . . . . . . . 15
⊢
〈𝑦, 𝑥〉 ∈ V | 
| 23 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V | 
| 24 | 22, 23 | breldm 5918 | . . . . . . . . . . . . . 14
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 → 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹) | 
| 25 | 24 | pm4.71ri 560 | . . . . . . . . . . . . 13
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ (〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧)) | 
| 26 |  | brtpos 8261 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧)) | 
| 27 | 26 | elv 3484 | . . . . . . . . . . . . 13
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧) | 
| 28 | 25, 27 | bitr3i 277 | . . . . . . . . . . . 12
⊢
((〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧) ↔ 〈𝑥, 𝑦〉𝐹𝑧) | 
| 29 | 21, 28 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 〈𝑥, 𝑦〉𝐹𝑧)) | 
| 30 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧)) | 
| 31 | 29, 30 | bitr4d 282 | . . . . . . . . . 10
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) | 
| 32 | 31 | exlimivv 1931 | . . . . . . . . 9
⊢
(∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) | 
| 33 | 9, 32 | sylbi 217 | . . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) | 
| 34 |  | iba 527 | . . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
(𝑤𝐹𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) | 
| 35 | 33, 34 | bitrd 279 | . . . . . . 7
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) | 
| 36 | 7, 8, 35 | pm5.21nii 378 | . . . . . 6
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))) | 
| 37 |  | elsni 4642 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} → 𝑤 = ∅) | 
| 38 | 37 | sneqd 4637 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {∅} → {𝑤} = {∅}) | 
| 39 | 38 | cnveqd 5885 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ◡{∅}) | 
| 40 |  | cnvsn0 6229 | . . . . . . . . . . . . . 14
⊢ ◡{∅} = ∅ | 
| 41 | 39, 40 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ∅) | 
| 42 | 41 | unieqd 4919 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∪
∅) | 
| 43 |  | uni0 4934 | . . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ | 
| 44 | 42, 43 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∅) | 
| 45 | 44 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅tpos 𝐹𝑧)) | 
| 46 |  | brtpos0 8259 | . . . . . . . . . . 11
⊢ (𝑧 ∈ V → (∅tpos
𝐹𝑧 ↔ ∅𝐹𝑧)) | 
| 47 | 46 | elv 3484 | . . . . . . . . . 10
⊢
(∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧) | 
| 48 | 45, 47 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅𝐹𝑧)) | 
| 49 | 37 | breq1d 5152 | . . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (𝑤𝐹𝑧 ↔ ∅𝐹𝑧)) | 
| 50 | 48, 49 | bitr4d 282 | . . . . . . . 8
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ 𝑤𝐹𝑧)) | 
| 51 | 50 | pm5.32i 574 | . . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧)) | 
| 52 | 51 | biancomi 462 | . . . . . 6
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) | 
| 53 | 36, 52 | orbi12i 914 | . . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) | 
| 54 |  | andir 1010 | . . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) | 
| 55 |  | andi 1009 | . . . . 5
⊢ ((𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) | 
| 56 | 53, 54, 55 | 3bitr4i 303 | . . . 4
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) | 
| 57 |  | elun 4152 | . . . . 5
⊢ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ↔ (𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅})) | 
| 58 | 57 | anbi1i 624 | . . . 4
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) | 
| 59 |  | brxp 5733 | . . . . . . 7
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ ((V × V) ∪
{∅}) ∧ 𝑧 ∈
V)) | 
| 60 | 23, 59 | mpbiran2 710 | . . . . . 6
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ 𝑤 ∈ ((V × V) ∪
{∅})) | 
| 61 |  | elun 4152 | . . . . . 6
⊢ (𝑤 ∈ ((V × V) ∪
{∅}) ↔ (𝑤 ∈
(V × V) ∨ 𝑤 ∈
{∅})) | 
| 62 | 60, 61 | bitri 275 | . . . . 5
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈
{∅})) | 
| 63 | 62 | anbi2i 623 | . . . 4
⊢ ((𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) | 
| 64 | 56, 58, 63 | 3bitr4i 303 | . . 3
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) | 
| 65 |  | brtpos2 8258 | . . . 4
⊢ (𝑧 ∈ V → (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) | 
| 66 | 65 | elv 3484 | . . 3
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) | 
| 67 |  | brin 5194 | . . 3
⊢ (𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) | 
| 68 | 64, 66, 67 | 3bitr4i 303 | . 2
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ 𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧) | 
| 69 | 1, 2, 68 | eqbrriv 5800 | 1
⊢ tpos tpos
𝐹 = (𝐹 ∩ (((V × V) ∪ {∅})
× V)) |