Proof of Theorem setsid
Step | Hyp | Ref
| Expression |
1 | | setsval 16507 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet 〈(𝐸‘ndx), 𝐶〉) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) |
2 | 1 | fveq2d 6668 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}))) |
3 | | setsid.e |
. . 3
⊢ 𝐸 = Slot (𝐸‘ndx) |
4 | | resexg 5892 |
. . . . 5
⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
5 | 4 | adantr 483 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
6 | | snex 5323 |
. . . 4
⊢
{〈(𝐸‘ndx), 𝐶〉} ∈ V |
7 | | unexg 7466 |
. . . 4
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧
{〈(𝐸‘ndx), 𝐶〉} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ∈
V) |
8 | 5, 6, 7 | sylancl 588 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ∈ V) |
9 | 3, 8 | strfvnd 16496 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
10 | | fvex 6677 |
. . . . . 6
⊢ (𝐸‘ndx) ∈
V |
11 | 10 | snid 4594 |
. . . . 5
⊢ (𝐸‘ndx) ∈ {(𝐸‘ndx)} |
12 | | fvres 6683 |
. . . . 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 5860 |
. . . . . . . . 9
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) |
15 | | incom 4177 |
. . . . . . . . . . . 12
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
({(𝐸‘ndx)} ∩ (V
∖ {(𝐸‘ndx)})) |
16 | | disjdif 4420 |
. . . . . . . . . . . 12
⊢ ({(𝐸‘ndx)} ∩ (V ∖
{(𝐸‘ndx)})) =
∅ |
17 | 15, 16 | eqtri 2844 |
. . . . . . . . . . 11
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
∅ |
18 | 17 | reseq2i 5844 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾
∅) |
19 | | res0 5851 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ∅) =
∅ |
20 | 18, 19 | eqtri 2844 |
. . . . . . . . 9
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) =
∅ |
21 | 14, 20 | eqtri 2844 |
. . . . . . . 8
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) =
∅ |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅) |
23 | | elex 3512 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
24 | 23 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V) |
25 | | opelxpi 5586 |
. . . . . . . . . 10
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
26 | 10, 24, 25 | sylancr 589 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
27 | | opex 5348 |
. . . . . . . . . 10
⊢
〈(𝐸‘ndx),
𝐶〉 ∈
V |
28 | 27 | relsn 5671 |
. . . . . . . . 9
⊢ (Rel
{〈(𝐸‘ndx), 𝐶〉} ↔ 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
29 | 26, 28 | sylibr 236 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {〈(𝐸‘ndx), 𝐶〉}) |
30 | | dmsnopss 6065 |
. . . . . . . 8
⊢ dom
{〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)} |
31 | | relssres 5887 |
. . . . . . . 8
⊢ ((Rel
{〈(𝐸‘ndx), 𝐶〉} ∧ dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
32 | 29, 30, 31 | sylancl 588 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
33 | 22, 32 | uneq12d 4139 |
. . . . . 6
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)})) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉})) |
34 | | resundir 5862 |
. . . . . 6
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪
({〈(𝐸‘ndx),
𝐶〉} ↾ {(𝐸‘ndx)})) |
35 | | un0 4343 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = {〈(𝐸‘ndx), 𝐶〉} |
36 | | uncom 4128 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉}) |
37 | 35, 36 | eqtr3i 2846 |
. . . . . 6
⊢
{〈(𝐸‘ndx), 𝐶〉} = (∅ ∪ {〈(𝐸‘ndx), 𝐶〉}) |
38 | 33, 34, 37 | 3eqtr4g 2881 |
. . . . 5
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
39 | 38 | fveq1d 6666 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
40 | 13, 39 | syl5eqr 2870 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
41 | 10 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ V) |
42 | | fvsng 6936 |
. . . 4
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
43 | 41, 42 | sylancom 590 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
44 | 40, 43 | eqtrd 2856 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = 𝐶) |
45 | 2, 9, 44 | 3eqtrrd 2861 |
1
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) |