Proof of Theorem setsid
Step | Hyp | Ref
| Expression |
1 | | setsval 16347 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet 〈(𝐸‘ndx), 𝐶〉) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) |
2 | 1 | fveq2d 6547 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}))) |
3 | | setsid.e |
. . 3
⊢ 𝐸 = Slot (𝐸‘ndx) |
4 | | resexg 5784 |
. . . . 5
⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
6 | | snex 5228 |
. . . 4
⊢
{〈(𝐸‘ndx), 𝐶〉} ∈ V |
7 | | unexg 7334 |
. . . 4
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧
{〈(𝐸‘ndx), 𝐶〉} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ∈
V) |
8 | 5, 6, 7 | sylancl 586 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ∈ V) |
9 | 3, 8 | strfvnd 16336 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
10 | | fvex 6556 |
. . . . . 6
⊢ (𝐸‘ndx) ∈
V |
11 | 10 | snid 4510 |
. . . . 5
⊢ (𝐸‘ndx) ∈ {(𝐸‘ndx)} |
12 | | fvres 6562 |
. . . . 5
⊢ ((𝐸‘ndx) ∈ {(𝐸‘ndx)} → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) |
14 | | resres 5752 |
. . . . . . . . 9
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) |
15 | | incom 4103 |
. . . . . . . . . . . 12
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
({(𝐸‘ndx)} ∩ (V
∖ {(𝐸‘ndx)})) |
16 | | disjdif 4339 |
. . . . . . . . . . . 12
⊢ ({(𝐸‘ndx)} ∩ (V ∖
{(𝐸‘ndx)})) =
∅ |
17 | 15, 16 | eqtri 2819 |
. . . . . . . . . . 11
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
∅ |
18 | 17 | reseq2i 5736 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾
∅) |
19 | | res0 5743 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ∅) =
∅ |
20 | 18, 19 | eqtri 2819 |
. . . . . . . . 9
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) =
∅ |
21 | 14, 20 | eqtri 2819 |
. . . . . . . 8
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) =
∅ |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅) |
23 | | elex 3455 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
24 | 23 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V) |
25 | | opelxpi 5485 |
. . . . . . . . . 10
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
26 | 10, 24, 25 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
27 | | opex 5253 |
. . . . . . . . . 10
⊢
〈(𝐸‘ndx),
𝐶〉 ∈
V |
28 | 27 | relsn 5568 |
. . . . . . . . 9
⊢ (Rel
{〈(𝐸‘ndx), 𝐶〉} ↔ 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
29 | 26, 28 | sylibr 235 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {〈(𝐸‘ndx), 𝐶〉}) |
30 | | dmsnopss 5951 |
. . . . . . . 8
⊢ dom
{〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)} |
31 | | relssres 5779 |
. . . . . . . 8
⊢ ((Rel
{〈(𝐸‘ndx), 𝐶〉} ∧ dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
32 | 29, 30, 31 | sylancl 586 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
33 | 22, 32 | uneq12d 4065 |
. . . . . 6
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)})) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉})) |
34 | | resundir 5754 |
. . . . . 6
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪
({〈(𝐸‘ndx),
𝐶〉} ↾ {(𝐸‘ndx)})) |
35 | | un0 4268 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = {〈(𝐸‘ndx), 𝐶〉} |
36 | | uncom 4054 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉}) |
37 | 35, 36 | eqtr3i 2821 |
. . . . . 6
⊢
{〈(𝐸‘ndx), 𝐶〉} = (∅ ∪ {〈(𝐸‘ndx), 𝐶〉}) |
38 | 33, 34, 37 | 3eqtr4g 2856 |
. . . . 5
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
39 | 38 | fveq1d 6545 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
40 | 13, 39 | syl5eqr 2845 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
41 | 10 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ V) |
42 | | fvsng 6810 |
. . . 4
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
43 | 41, 42 | sylancom 588 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
44 | 40, 43 | eqtrd 2831 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = 𝐶) |
45 | 2, 9, 44 | 3eqtrrd 2836 |
1
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) |