Step | Hyp | Ref
| Expression |
1 | | reltpos 8166 |
. 2
⊢ Rel tpos
tpos 𝐹 |
2 | | relinxp 5774 |
. 2
⊢ Rel
(𝐹 ∩ (((V × V)
∪ {∅}) × V)) |
3 | | relcnv 6060 |
. . . . . . . . 9
⊢ Rel ◡dom tpos 𝐹 |
4 | | df-rel 5644 |
. . . . . . . . 9
⊢ (Rel
◡dom tpos 𝐹 ↔ ◡dom tpos 𝐹 ⊆ (V × V)) |
5 | 3, 4 | mpbi 229 |
. . . . . . . 8
⊢ ◡dom tpos 𝐹 ⊆ (V × V) |
6 | | simpl 484 |
. . . . . . . 8
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ ◡dom tpos 𝐹) |
7 | 5, 6 | sselid 3946 |
. . . . . . 7
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ (V × V)) |
8 | | simpr 486 |
. . . . . . 7
⊢ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) → 𝑤 ∈ (V ×
V)) |
9 | | elvv 5710 |
. . . . . . . . 9
⊢ (𝑤 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩) |
10 | | eleq1 2822 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹)) |
11 | | vex 3451 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
12 | | vex 3451 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
13 | 11, 12 | opelcnv 5841 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹) |
14 | 10, 13 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹)) |
15 | | sneq 4600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → {𝑤} = {⟨𝑥, 𝑦⟩}) |
16 | 15 | cnveqd 5835 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ◡{𝑤} = ◡{⟨𝑥, 𝑦⟩}) |
17 | 16 | unieqd 4883 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪
◡{𝑤} = ∪ ◡{⟨𝑥, 𝑦⟩}) |
18 | | opswap 6185 |
. . . . . . . . . . . . . . 15
⊢ ∪ ◡{⟨𝑥, 𝑦⟩} = ⟨𝑦, 𝑥⟩ |
19 | 17, 18 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪
◡{𝑤} = ⟨𝑦, 𝑥⟩) |
20 | 19 | breq1d 5119 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (∪
◡{𝑤}tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧)) |
21 | 14, 20 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧))) |
22 | | opex 5425 |
. . . . . . . . . . . . . . 15
⊢
⟨𝑦, 𝑥⟩ ∈ V |
23 | | vex 3451 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
24 | 22, 23 | breldm 5868 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 → ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹) |
25 | 24 | pm4.71ri 562 |
. . . . . . . . . . . . 13
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧)) |
26 | | brtpos 8170 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
27 | 26 | elv 3453 |
. . . . . . . . . . . . 13
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧) |
28 | 25, 27 | bitr3i 277 |
. . . . . . . . . . . 12
⊢
((⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧) |
29 | 21, 28 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
30 | | breq1 5112 |
. . . . . . . . . . 11
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
31 | 29, 30 | bitr4d 282 |
. . . . . . . . . 10
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
32 | 31 | exlimivv 1936 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
33 | 9, 32 | sylbi 216 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
34 | | iba 529 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
(𝑤𝐹𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
35 | 33, 34 | bitrd 279 |
. . . . . . 7
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
36 | 7, 8, 35 | pm5.21nii 380 |
. . . . . 6
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))) |
37 | | elsni 4607 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} → 𝑤 = ∅) |
38 | 37 | sneqd 4602 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {∅} → {𝑤} = {∅}) |
39 | 38 | cnveqd 5835 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ◡{∅}) |
40 | | cnvsn0 6166 |
. . . . . . . . . . . . . 14
⊢ ◡{∅} = ∅ |
41 | 39, 40 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ∅) |
42 | 41 | unieqd 4883 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∪
∅) |
43 | | uni0 4900 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∅) |
45 | 44 | breq1d 5119 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅tpos 𝐹𝑧)) |
46 | | brtpos0 8168 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (∅tpos
𝐹𝑧 ↔ ∅𝐹𝑧)) |
47 | 46 | elv 3453 |
. . . . . . . . . 10
⊢
(∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧) |
48 | 45, 47 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅𝐹𝑧)) |
49 | 37 | breq1d 5119 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (𝑤𝐹𝑧 ↔ ∅𝐹𝑧)) |
50 | 48, 49 | bitr4d 282 |
. . . . . . . 8
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ 𝑤𝐹𝑧)) |
51 | 50 | pm5.32i 576 |
. . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧)) |
52 | 51 | biancomi 464 |
. . . . . 6
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) |
53 | 36, 52 | orbi12i 914 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
54 | | andir 1008 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
55 | | andi 1007 |
. . . . 5
⊢ ((𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
56 | 53, 54, 55 | 3bitr4i 303 |
. . . 4
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
57 | | elun 4112 |
. . . . 5
⊢ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ↔ (𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅})) |
58 | 57 | anbi1i 625 |
. . . 4
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
59 | | brxp 5685 |
. . . . . . 7
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ ((V × V) ∪
{∅}) ∧ 𝑧 ∈
V)) |
60 | 23, 59 | mpbiran2 709 |
. . . . . 6
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ 𝑤 ∈ ((V × V) ∪
{∅})) |
61 | | elun 4112 |
. . . . . 6
⊢ (𝑤 ∈ ((V × V) ∪
{∅}) ↔ (𝑤 ∈
(V × V) ∨ 𝑤 ∈
{∅})) |
62 | 60, 61 | bitri 275 |
. . . . 5
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈
{∅})) |
63 | 62 | anbi2i 624 |
. . . 4
⊢ ((𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
64 | 56, 58, 63 | 3bitr4i 303 |
. . 3
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
65 | | brtpos2 8167 |
. . . 4
⊢ (𝑧 ∈ V → (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
66 | 65 | elv 3453 |
. . 3
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
67 | | brin 5161 |
. . 3
⊢ (𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
68 | 64, 66, 67 | 3bitr4i 303 |
. 2
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ 𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧) |
69 | 1, 2, 68 | eqbrriv 5751 |
1
⊢ tpos tpos
𝐹 = (𝐹 ∩ (((V × V) ∪ {∅})
× V)) |