Step | Hyp | Ref
| Expression |
1 | | df-tpos 8161 |
. . 3
⊢ tpos
𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) |
2 | | relcnv 6060 |
. . . . . . 7
⊢ Rel ◡dom 𝐹 |
3 | | df-rel 5644 |
. . . . . . 7
⊢ (Rel
◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V)) |
4 | 2, 3 | mpbi 229 |
. . . . . 6
⊢ ◡dom 𝐹 ⊆ (V × V) |
5 | | unss1 4143 |
. . . . . 6
⊢ (◡dom 𝐹 ⊆ (V × V) → (◡dom 𝐹 ∪ {∅}) ⊆ ((V × V)
∪ {∅})) |
6 | | resmpt 5995 |
. . . . . 6
⊢ ((◡dom 𝐹 ∪ {∅}) ⊆ ((V × V)
∪ {∅}) → ((𝑥
∈ ((V × V) ∪ {∅}) ↦ ∪
◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) |
7 | 4, 5, 6 | mp2b 10 |
. . . . 5
⊢ ((𝑥 ∈ ((V × V) ∪
{∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) = (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) |
8 | | resss 5966 |
. . . . 5
⊢ ((𝑥 ∈ ((V × V) ∪
{∅}) ↦ ∪ ◡{𝑥}) ↾ (◡dom 𝐹 ∪ {∅})) ⊆ (𝑥 ∈ ((V × V) ∪
{∅}) ↦ ∪ ◡{𝑥}) |
9 | 7, 8 | eqsstrri 3983 |
. . . 4
⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥}) |
10 | | coss2 5816 |
. . . 4
⊢ ((𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}) ⊆ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥}) → (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥}))) |
11 | 9, 10 | ax-mp 5 |
. . 3
⊢ (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) |
12 | 1, 11 | eqsstri 3982 |
. 2
⊢ tpos
𝐹 ⊆ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) |
13 | | relco 6064 |
. . 3
⊢ Rel
(𝐹 ∘ (𝑥 ∈ ((V × V) ∪
{∅}) ↦ ∪ ◡{𝑥})) |
14 | | vex 3451 |
. . . . 5
⊢ 𝑦 ∈ V |
15 | | vex 3451 |
. . . . 5
⊢ 𝑧 ∈ V |
16 | 14, 15 | opelco 5831 |
. . . 4
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) ↔ ∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧)) |
17 | | vex 3451 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
18 | | eleq1 2822 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ((V × V) ∪ {∅})
↔ 𝑦 ∈ ((V ×
V) ∪ {∅}))) |
19 | | sneq 4600 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
20 | 19 | cnveqd 5835 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ◡{𝑥} = ◡{𝑦}) |
21 | 20 | unieqd 4883 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ∪ ◡{𝑥} = ∪ ◡{𝑦}) |
22 | 21 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑧 = ∪ ◡{𝑥} ↔ 𝑧 = ∪ ◡{𝑦})) |
23 | 18, 22 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ((V × V) ∪ {∅}) ∧
𝑧 = ∪ ◡{𝑥}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧
𝑧 = ∪ ◡{𝑦}))) |
24 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑧 = ∪ ◡{𝑦} ↔ 𝑤 = ∪ ◡{𝑦})) |
25 | 24 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((𝑦 ∈ ((V × V) ∪ {∅}) ∧
𝑧 = ∪ ◡{𝑦}) ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧
𝑤 = ∪ ◡{𝑦}))) |
26 | | df-mpt 5193 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((V × V) ∪
{∅}) ↦ ∪ ◡{𝑥}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ((V × V) ∪ {∅}) ∧
𝑧 = ∪ ◡{𝑥})} |
27 | 14, 17, 23, 25, 26 | brab 5504 |
. . . . . . . 8
⊢ (𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ↔ (𝑦 ∈ ((V × V) ∪ {∅}) ∧
𝑤 = ∪ ◡{𝑦})) |
28 | | simplr 768 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 = ∪ ◡{𝑦}) |
29 | 17, 15 | breldm 5868 |
. . . . . . . . . . . . 13
⊢ (𝑤𝐹𝑧 → 𝑤 ∈ dom 𝐹) |
30 | 29 | adantl 483 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤 ∈ dom 𝐹) |
31 | 28, 30 | eqeltrrd 2835 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦} ∈ dom 𝐹) |
32 | | elvv 5710 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (V × V) ↔
∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩) |
33 | | opswap 6185 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ ◡{⟨𝑧, 𝑤⟩} = ⟨𝑤, 𝑧⟩ |
34 | 33 | eleq1i 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹) |
35 | 15, 17 | opelcnv 5841 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹 ↔ ⟨𝑤, 𝑧⟩ ∈ dom 𝐹) |
36 | 34, 35 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
⊢ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹) |
37 | | sneq 4600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → {𝑦} = {⟨𝑧, 𝑤⟩}) |
38 | 37 | cnveqd 5835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ◡{𝑦} = ◡{⟨𝑧, 𝑤⟩}) |
39 | 38 | unieqd 4883 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ∪
◡{𝑦} = ∪ ◡{⟨𝑧, 𝑤⟩}) |
40 | 39 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪
◡{𝑦} ∈ dom 𝐹 ↔ ∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹)) |
41 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ◡dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹)) |
42 | 40, 41 | bibi12d 346 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ((∪
◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹) ↔ (∪ ◡{⟨𝑧, 𝑤⟩} ∈ dom 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ ◡dom 𝐹))) |
43 | 36, 42 | mpbiri 258 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (∪
◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹)) |
44 | 43 | exlimivv 1936 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (∪
◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹)) |
45 | 32, 44 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (V × V) →
(∪ ◡{𝑦} ∈ dom 𝐹 ↔ 𝑦 ∈ ◡dom 𝐹)) |
46 | 45 | biimpcd 249 |
. . . . . . . . . . . 12
⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ ◡dom 𝐹)) |
47 | | elun1 4140 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ◡dom 𝐹 → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})) |
48 | 46, 47 | syl6 35 |
. . . . . . . . . . 11
⊢ (∪ ◡{𝑦} ∈ dom 𝐹 → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))) |
49 | 31, 48 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))) |
50 | | elun2 4141 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ {∅} → 𝑦 ∈ (◡dom 𝐹 ∪ {∅}))) |
52 | | simpll 766 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ ((V × V) ∪
{∅})) |
53 | | elun 4112 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((V × V) ∪
{∅}) ↔ (𝑦 ∈
(V × V) ∨ 𝑦 ∈
{∅})) |
54 | 52, 53 | sylib 217 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (V × V) ∨ 𝑦 ∈ {∅})) |
55 | 49, 51, 54 | mpjaod 859 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑦 ∈ (◡dom 𝐹 ∪ {∅})) |
56 | | simpr 486 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → 𝑤𝐹𝑧) |
57 | 28, 56 | eqbrtrrd 5133 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → ∪ ◡{𝑦}𝐹𝑧) |
58 | 55, 57 | jca 513 |
. . . . . . . 8
⊢ (((𝑦 ∈ ((V × V) ∪
{∅}) ∧ 𝑤 = ∪ ◡{𝑦}) ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)) |
59 | 27, 58 | sylanb 582 |
. . . . . . 7
⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)) |
60 | | brtpos2 8167 |
. . . . . . . 8
⊢ (𝑧 ∈ V → (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧))) |
61 | 15, 60 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦tpos 𝐹𝑧 ↔ (𝑦 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑦}𝐹𝑧)) |
62 | 59, 61 | sylibr 233 |
. . . . . 6
⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → 𝑦tpos 𝐹𝑧) |
63 | | df-br 5110 |
. . . . . 6
⊢ (𝑦tpos 𝐹𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹) |
64 | 62, 63 | sylib 217 |
. . . . 5
⊢ ((𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹) |
65 | 64 | exlimiv 1934 |
. . . 4
⊢
(∃𝑤(𝑦(𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})𝑤 ∧ 𝑤𝐹𝑧) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹) |
66 | 16, 65 | sylbi 216 |
. . 3
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) → ⟨𝑦, 𝑧⟩ ∈ tpos 𝐹) |
67 | 13, 66 | relssi 5747 |
. 2
⊢ (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) ⊆ tpos 𝐹 |
68 | 12, 67 | eqssi 3964 |
1
⊢ tpos
𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅})
↦ ∪ ◡{𝑥})) |