Step | Hyp | Ref
| Expression |
1 | | reltpos 7357 |
. 2
⊢ Rel tpos
tpos 𝐹 |
2 | | inss2 3834 |
. . 3
⊢ (𝐹 ∩ (((V × V) ∪
{∅}) × V)) ⊆ (((V × V) ∪ {∅}) ×
V) |
3 | | relxp 5227 |
. . 3
⊢ Rel (((V
× V) ∪ {∅}) × V) |
4 | | relss 5206 |
. . 3
⊢ ((𝐹 ∩ (((V × V) ∪
{∅}) × V)) ⊆ (((V × V) ∪ {∅}) × V)
→ (Rel (((V × V) ∪ {∅}) × V) → Rel (𝐹 ∩ (((V × V) ∪
{∅}) × V)))) |
5 | 2, 3, 4 | mp2 9 |
. 2
⊢ Rel
(𝐹 ∩ (((V × V)
∪ {∅}) × V)) |
6 | | relcnv 5503 |
. . . . . . . . 9
⊢ Rel ◡dom tpos 𝐹 |
7 | | df-rel 5121 |
. . . . . . . . 9
⊢ (Rel
◡dom tpos 𝐹 ↔ ◡dom tpos 𝐹 ⊆ (V × V)) |
8 | 6, 7 | mpbi 220 |
. . . . . . . 8
⊢ ◡dom tpos 𝐹 ⊆ (V × V) |
9 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ ◡dom tpos 𝐹) |
10 | 8, 9 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ (V × V)) |
11 | | simpr 477 |
. . . . . . 7
⊢ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) → 𝑤 ∈ (V ×
V)) |
12 | | elvv 5177 |
. . . . . . . . 9
⊢ (𝑤 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉) |
13 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ ◡dom tpos 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ ◡dom tpos 𝐹)) |
14 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
15 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
16 | 14, 15 | opelcnv 5304 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ ◡dom tpos 𝐹 ↔ 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹) |
17 | 13, 16 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ ◡dom tpos 𝐹 ↔ 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹)) |
18 | | sneq 4187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑥, 𝑦〉 → {𝑤} = {〈𝑥, 𝑦〉}) |
19 | 18 | cnveqd 5298 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ◡{𝑤} = ◡{〈𝑥, 𝑦〉}) |
20 | 19 | unieqd 4446 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ∪
◡{𝑤} = ∪ ◡{〈𝑥, 𝑦〉}) |
21 | | opswap 5622 |
. . . . . . . . . . . . . . 15
⊢ ∪ ◡{〈𝑥, 𝑦〉} = 〈𝑦, 𝑥〉 |
22 | 20, 21 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ∪
◡{𝑤} = 〈𝑦, 𝑥〉) |
23 | 22 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (∪
◡{𝑤}tpos 𝐹𝑧 ↔ 〈𝑦, 𝑥〉tpos 𝐹𝑧)) |
24 | 17, 23 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧))) |
25 | | opex 4932 |
. . . . . . . . . . . . . . 15
⊢
〈𝑦, 𝑥〉 ∈ V |
26 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
27 | 25, 26 | breldm 5329 |
. . . . . . . . . . . . . 14
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 → 〈𝑦, 𝑥〉 ∈ dom tpos 𝐹) |
28 | 27 | pm4.71ri 665 |
. . . . . . . . . . . . 13
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ (〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧)) |
29 | | brtpos 7361 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧)) |
30 | 26, 29 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(〈𝑦, 𝑥〉tpos 𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧) |
31 | 28, 30 | bitr3i 266 |
. . . . . . . . . . . 12
⊢
((〈𝑦, 𝑥〉 ∈ dom tpos 𝐹 ∧ 〈𝑦, 𝑥〉tpos 𝐹𝑧) ↔ 〈𝑥, 𝑦〉𝐹𝑧) |
32 | 24, 31 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 〈𝑥, 𝑦〉𝐹𝑧)) |
33 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤𝐹𝑧 ↔ 〈𝑥, 𝑦〉𝐹𝑧)) |
34 | 32, 33 | bitr4d 271 |
. . . . . . . . . 10
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
35 | 34 | exlimivv 1860 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
36 | 12, 35 | sylbi 207 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
37 | | iba 524 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
(𝑤𝐹𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
38 | 36, 37 | bitrd 268 |
. . . . . . 7
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
39 | 10, 11, 38 | pm5.21nii 368 |
. . . . . 6
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))) |
40 | | elsni 4194 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} → 𝑤 = ∅) |
41 | 40 | sneqd 4189 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {∅} → {𝑤} = {∅}) |
42 | 41 | cnveqd 5298 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ◡{∅}) |
43 | | cnvsn0 5603 |
. . . . . . . . . . . . . 14
⊢ ◡{∅} = ∅ |
44 | 42, 43 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ∅) |
45 | 44 | unieqd 4446 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∪
∅) |
46 | | uni0 4465 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
47 | 45, 46 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∅) |
48 | 47 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅tpos 𝐹𝑧)) |
49 | | brtpos0 7359 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (∅tpos
𝐹𝑧 ↔ ∅𝐹𝑧)) |
50 | 26, 49 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧) |
51 | 48, 50 | syl6bb 276 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅𝐹𝑧)) |
52 | 40 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (𝑤𝐹𝑧 ↔ ∅𝐹𝑧)) |
53 | 51, 52 | bitr4d 271 |
. . . . . . . 8
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ 𝑤𝐹𝑧)) |
54 | 53 | pm5.32i 669 |
. . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧)) |
55 | | ancom 466 |
. . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) |
56 | 54, 55 | bitri 264 |
. . . . . 6
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) |
57 | 39, 56 | orbi12i 543 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
58 | | andir 912 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
59 | | andi 911 |
. . . . 5
⊢ ((𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
60 | 57, 58, 59 | 3bitr4i 292 |
. . . 4
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
61 | | elun 3753 |
. . . . 5
⊢ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ↔ (𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅})) |
62 | 61 | anbi1i 731 |
. . . 4
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
63 | | brxp 5147 |
. . . . . . 7
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ ((V × V) ∪
{∅}) ∧ 𝑧 ∈
V)) |
64 | 26, 63 | mpbiran2 954 |
. . . . . 6
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ 𝑤 ∈ ((V × V) ∪
{∅})) |
65 | | elun 3753 |
. . . . . 6
⊢ (𝑤 ∈ ((V × V) ∪
{∅}) ↔ (𝑤 ∈
(V × V) ∨ 𝑤 ∈
{∅})) |
66 | 64, 65 | bitri 264 |
. . . . 5
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈
{∅})) |
67 | 66 | anbi2i 730 |
. . . 4
⊢ ((𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
68 | 60, 62, 67 | 3bitr4i 292 |
. . 3
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
69 | | brtpos2 7358 |
. . . 4
⊢ (𝑧 ∈ V → (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
70 | 26, 69 | ax-mp 5 |
. . 3
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
71 | | brin 4704 |
. . 3
⊢ (𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
72 | 68, 70, 71 | 3bitr4i 292 |
. 2
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ 𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧) |
73 | 1, 5, 72 | eqbrriv 5215 |
1
⊢ tpos tpos
𝐹 = (𝐹 ∩ (((V × V) ∪ {∅})
× V)) |