Proof of Theorem setsid
| Step | Hyp | Ref
| Expression |
| 1 | | setsval 17204 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet 〈(𝐸‘ndx), 𝐶〉) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) |
| 2 | 1 | fveq2d 6910 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}))) |
| 3 | | setsid.e |
. . 3
⊢ 𝐸 = Slot (𝐸‘ndx) |
| 4 | | resexg 6045 |
. . . . 5
⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
| 6 | | snex 5436 |
. . . 4
⊢
{〈(𝐸‘ndx), 𝐶〉} ∈ V |
| 7 | | unexg 7763 |
. . . 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 17222 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
| 10 | | fvex 6919 |
. . . . . 6
⊢ (𝐸‘ndx) ∈
V |
| 11 | 10 | snid 4662 |
. . . . 5
⊢ (𝐸‘ndx) ∈ {(𝐸‘ndx)} |
| 12 | | fvres 6925 |
. . . . 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 6010 |
. . . . . . . . 9
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) |
| 15 | | disjdifr 4473 |
. . . . . . . . . . 11
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
∅ |
| 16 | 15 | reseq2i 5994 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾
∅) |
| 17 | | res0 6001 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ∅) =
∅ |
| 18 | 16, 17 | eqtri 2765 |
. . . . . . . . 9
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) =
∅ |
| 19 | 14, 18 | eqtri 2765 |
. . . . . . . 8
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) =
∅ |
| 20 | 19 | a1i 11 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅) |
| 21 | | elex 3501 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
| 22 | 21 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V) |
| 23 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
| 24 | 10, 22, 23 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
| 25 | | opex 5469 |
. . . . . . . . . 10
⊢
〈(𝐸‘ndx),
𝐶〉 ∈
V |
| 26 | 25 | relsn 5814 |
. . . . . . . . 9
⊢ (Rel
{〈(𝐸‘ndx), 𝐶〉} ↔ 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
| 27 | 24, 26 | sylibr 234 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {〈(𝐸‘ndx), 𝐶〉}) |
| 28 | | dmsnopss 6234 |
. . . . . . . 8
⊢ dom
{〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)} |
| 29 | | relssres 6040 |
. . . . . . . 8
⊢ ((Rel
{〈(𝐸‘ndx), 𝐶〉} ∧ dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
| 30 | 27, 28, 29 | sylancl 586 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
| 31 | 20, 30 | uneq12d 4169 |
. . . . . 6
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)})) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉})) |
| 32 | | resundir 6012 |
. . . . . 6
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪
({〈(𝐸‘ndx),
𝐶〉} ↾ {(𝐸‘ndx)})) |
| 33 | | un0 4394 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = {〈(𝐸‘ndx), 𝐶〉} |
| 34 | | uncom 4158 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉}) |
| 35 | 33, 34 | eqtr3i 2767 |
. . . . . 6
⊢
{〈(𝐸‘ndx), 𝐶〉} = (∅ ∪ {〈(𝐸‘ndx), 𝐶〉}) |
| 36 | 31, 32, 35 | 3eqtr4g 2802 |
. . . . 5
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
| 37 | 36 | fveq1d 6908 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
| 38 | 13, 37 | eqtr3id 2791 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
| 39 | 10 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ V) |
| 40 | | fvsng 7200 |
. . . 4
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
| 41 | 39, 40 | sylancom 588 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
| 42 | 38, 41 | eqtrd 2777 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = 𝐶) |
| 43 | 2, 9, 42 | 3eqtrrd 2782 |
1
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) |