Step | Hyp | Ref
| Expression |
1 | | reltpos 6253 |
. 2
⊢ Rel tpos
tpos 𝐹 |
2 | | inss2 3358 |
. . 3
⊢ (𝐹 ∩ (((V × V) ∪
{∅}) × V)) ⊆ (((V × V) ∪ {∅}) ×
V) |
3 | | relxp 4737 |
. . 3
⊢ Rel (((V
× V) ∪ {∅}) × V) |
4 | | relss 4715 |
. . 3
⊢ ((𝐹 ∩ (((V × V) ∪
{∅}) × V)) ⊆ (((V × V) ∪ {∅}) × V)
→ (Rel (((V × V) ∪ {∅}) × V) → Rel (𝐹 ∩ (((V × V) ∪
{∅}) × V)))) |
5 | 2, 3, 4 | mp2 16 |
. 2
⊢ Rel
(𝐹 ∩ (((V × V)
∪ {∅}) × V)) |
6 | | relcnv 5008 |
. . . . . . . . 9
⊢ Rel ◡dom tpos 𝐹 |
7 | | df-rel 4635 |
. . . . . . . . 9
⊢ (Rel
◡dom tpos 𝐹 ↔ ◡dom tpos 𝐹 ⊆ (V × V)) |
8 | 6, 7 | mpbi 145 |
. . . . . . . 8
⊢ ◡dom tpos 𝐹 ⊆ (V × V) |
9 | | simpl 109 |
. . . . . . . 8
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ ◡dom tpos 𝐹) |
10 | 8, 9 | sselid 3155 |
. . . . . . 7
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) → 𝑤 ∈ (V × V)) |
11 | | simpr 110 |
. . . . . . 7
⊢ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) → 𝑤 ∈ (V ×
V)) |
12 | | elvv 4690 |
. . . . . . . . 9
⊢ (𝑤 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩) |
13 | | eleq1 2240 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹)) |
14 | | vex 2742 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
15 | | vex 2742 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
16 | 14, 15 | opelcnv 4811 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑥, 𝑦⟩ ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹) |
17 | 13, 16 | bitrdi 196 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ ◡dom tpos 𝐹 ↔ ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹)) |
18 | | sneq 3605 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → {𝑤} = {⟨𝑥, 𝑦⟩}) |
19 | 18 | cnveqd 4805 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ◡{𝑤} = ◡{⟨𝑥, 𝑦⟩}) |
20 | 19 | unieqd 3822 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪
◡{𝑤} = ∪ ◡{⟨𝑥, 𝑦⟩}) |
21 | | opswapg 5117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ∪ ◡{⟨𝑥, 𝑦⟩} = ⟨𝑦, 𝑥⟩) |
22 | 14, 15, 21 | mp2an 426 |
. . . . . . . . . . . . . . 15
⊢ ∪ ◡{⟨𝑥, 𝑦⟩} = ⟨𝑦, 𝑥⟩ |
23 | 20, 22 | eqtrdi 2226 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ∪
◡{𝑤} = ⟨𝑦, 𝑥⟩) |
24 | 23 | breq1d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (∪
◡{𝑤}tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧)) |
25 | 17, 24 | anbi12d 473 |
. . . . . . . . . . . 12
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧))) |
26 | 15, 14 | opex 4231 |
. . . . . . . . . . . . . . 15
⊢
⟨𝑦, 𝑥⟩ ∈ V |
27 | | vex 2742 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
28 | 26, 27 | breldm 4833 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 → ⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹) |
29 | 28 | pm4.71ri 392 |
. . . . . . . . . . . . 13
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ (⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧)) |
30 | | brtposg 6257 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ V ∧ 𝑥 ∈ V ∧ 𝑧 ∈ V) → (⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
31 | 15, 14, 27, 30 | mp3an 1337 |
. . . . . . . . . . . . 13
⊢
(⟨𝑦, 𝑥⟩tpos 𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧) |
32 | 29, 31 | bitr3i 186 |
. . . . . . . . . . . 12
⊢
((⟨𝑦, 𝑥⟩ ∈ dom tpos 𝐹 ∧ ⟨𝑦, 𝑥⟩tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧) |
33 | 25, 32 | bitrdi 196 |
. . . . . . . . . . 11
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
34 | | breq1 4008 |
. . . . . . . . . . 11
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤𝐹𝑧 ↔ ⟨𝑥, 𝑦⟩𝐹𝑧)) |
35 | 33, 34 | bitr4d 191 |
. . . . . . . . . 10
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
36 | 35 | exlimivv 1896 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦 𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
37 | 12, 36 | sylbi 121 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ 𝑤𝐹𝑧)) |
38 | | iba 300 |
. . . . . . . 8
⊢ (𝑤 ∈ (V × V) →
(𝑤𝐹𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
39 | 37, 38 | bitrd 188 |
. . . . . . 7
⊢ (𝑤 ∈ (V × V) →
((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)))) |
40 | 10, 11, 39 | pm5.21nii 704 |
. . . . . 6
⊢ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V))) |
41 | | elsni 3612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {∅} → 𝑤 = ∅) |
42 | 41 | sneqd 3607 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {∅} → {𝑤} = {∅}) |
43 | 42 | cnveqd 4805 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ◡{∅}) |
44 | | cnvsn0 5099 |
. . . . . . . . . . . . . 14
⊢ ◡{∅} = ∅ |
45 | 43, 44 | eqtrdi 2226 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {∅} → ◡{𝑤} = ∅) |
46 | 45 | unieqd 3822 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∪
∅) |
47 | | uni0 3838 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
48 | 46, 47 | eqtrdi 2226 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {∅} → ∪ ◡{𝑤} = ∅) |
49 | 48 | breq1d 4015 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅tpos 𝐹𝑧)) |
50 | | brtpos0 6255 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (∅tpos
𝐹𝑧 ↔ ∅𝐹𝑧)) |
51 | 27, 50 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∅tpos 𝐹𝑧 ↔ ∅𝐹𝑧) |
52 | 49, 51 | bitrdi 196 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ ∅𝐹𝑧)) |
53 | 41 | breq1d 4015 |
. . . . . . . . 9
⊢ (𝑤 ∈ {∅} → (𝑤𝐹𝑧 ↔ ∅𝐹𝑧)) |
54 | 52, 53 | bitr4d 191 |
. . . . . . . 8
⊢ (𝑤 ∈ {∅} → (∪ ◡{𝑤}tpos 𝐹𝑧 ↔ 𝑤𝐹𝑧)) |
55 | 54 | pm5.32i 454 |
. . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧)) |
56 | | ancom 266 |
. . . . . . 7
⊢ ((𝑤 ∈ {∅} ∧ 𝑤𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) |
57 | 55, 56 | bitri 184 |
. . . . . 6
⊢ ((𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅})) |
58 | 40, 57 | orbi12i 764 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
59 | | andir 819 |
. . . . 5
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ∨ (𝑤 ∈ {∅} ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
60 | | andi 818 |
. . . . 5
⊢ ((𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅})) ↔ ((𝑤𝐹𝑧 ∧ 𝑤 ∈ (V × V)) ∨ (𝑤𝐹𝑧 ∧ 𝑤 ∈ {∅}))) |
61 | 58, 59, 60 | 3bitr4i 212 |
. . . 4
⊢ (((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
62 | | elun 3278 |
. . . . 5
⊢ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ↔ (𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅})) |
63 | 62 | anbi1i 458 |
. . . 4
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ ((𝑤 ∈ ◡dom tpos 𝐹 ∨ 𝑤 ∈ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
64 | | brxp 4659 |
. . . . . . 7
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ ((V × V) ∪
{∅}) ∧ 𝑧 ∈
V)) |
65 | 27, 64 | mpbiran2 941 |
. . . . . 6
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ 𝑤 ∈ ((V × V) ∪
{∅})) |
66 | | elun 3278 |
. . . . . 6
⊢ (𝑤 ∈ ((V × V) ∪
{∅}) ↔ (𝑤 ∈
(V × V) ∨ 𝑤 ∈
{∅})) |
67 | 65, 66 | bitri 184 |
. . . . 5
⊢ (𝑤(((V × V) ∪ {∅})
× V)𝑧 ↔ (𝑤 ∈ (V × V) ∨ 𝑤 ∈
{∅})) |
68 | 67 | anbi2i 457 |
. . . 4
⊢ ((𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧) ↔ (𝑤𝐹𝑧 ∧ (𝑤 ∈ (V × V) ∨ 𝑤 ∈ {∅}))) |
69 | 61, 63, 68 | 3bitr4i 212 |
. . 3
⊢ ((𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧) ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
70 | | brtpos2 6254 |
. . . 4
⊢ (𝑧 ∈ V → (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧))) |
71 | 27, 70 | ax-mp 5 |
. . 3
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ (𝑤 ∈ (◡dom tpos 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑤}tpos 𝐹𝑧)) |
72 | | brin 4057 |
. . 3
⊢ (𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧 ↔ (𝑤𝐹𝑧 ∧ 𝑤(((V × V) ∪ {∅}) ×
V)𝑧)) |
73 | 69, 71, 72 | 3bitr4i 212 |
. 2
⊢ (𝑤tpos tpos 𝐹𝑧 ↔ 𝑤(𝐹 ∩ (((V × V) ∪ {∅})
× V))𝑧) |
74 | 1, 5, 73 | eqbrriv 4723 |
1
⊢ tpos tpos
𝐹 = (𝐹 ∩ (((V × V) ∪ {∅})
× V)) |