Proof of Theorem setsslid
Step | Hyp | Ref
| Expression |
1 | | setsslid.e |
. . . . 5
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) |
2 | 1 | simpri 112 |
. . . 4
⊢ (𝐸‘ndx) ∈
ℕ |
3 | | setsvala 12436 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ (𝐸‘ndx) ∈ ℕ ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet 〈(𝐸‘ndx), 𝐶〉) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) |
4 | 2, 3 | mp3an2 1320 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet 〈(𝐸‘ndx), 𝐶〉) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) |
5 | 4 | fveq2d 5498 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}))) |
6 | 1 | simpli 110 |
. . 3
⊢ 𝐸 = Slot (𝐸‘ndx) |
7 | | resexg 4929 |
. . . 4
⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V) |
8 | | simpr 109 |
. . . . . 6
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉) |
9 | | opexg 4211 |
. . . . . 6
⊢ (((𝐸‘ndx) ∈ ℕ ∧
𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ V) |
10 | 2, 8, 9 | sylancr 412 |
. . . . 5
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ V) |
11 | | snexg 4168 |
. . . . 5
⊢
(〈(𝐸‘ndx), 𝐶〉 ∈ V → {〈(𝐸‘ndx), 𝐶〉} ∈ V) |
12 | 10, 11 | syl 14 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → {〈(𝐸‘ndx), 𝐶〉} ∈ V) |
13 | | unexg 4426 |
. . . 4
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧
{〈(𝐸‘ndx), 𝐶〉} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ∈
V) |
14 | 7, 12, 13 | syl2an2r 590 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ∈ V) |
15 | 2 | a1i 9 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ ℕ) |
16 | 6, 14, 15 | strnfvnd 12425 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
17 | | snidg 3610 |
. . . . 5
⊢ ((𝐸‘ndx) ∈ ℕ
→ (𝐸‘ndx) ∈
{(𝐸‘ndx)}) |
18 | | fvres 5518 |
. . . . 5
⊢ ((𝐸‘ndx) ∈ {(𝐸‘ndx)} → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx))) |
19 | 2, 17, 18 | mp2b 8 |
. . . 4
⊢ ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) |
20 | | resres 4901 |
. . . . . . . . 9
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) |
21 | | incom 3319 |
. . . . . . . . . . . 12
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
({(𝐸‘ndx)} ∩ (V
∖ {(𝐸‘ndx)})) |
22 | | disjdif 3486 |
. . . . . . . . . . . 12
⊢ ({(𝐸‘ndx)} ∩ (V ∖
{(𝐸‘ndx)})) =
∅ |
23 | 21, 22 | eqtri 2191 |
. . . . . . . . . . 11
⊢ ((V
∖ {(𝐸‘ndx)})
∩ {(𝐸‘ndx)}) =
∅ |
24 | 23 | reseq2i 4886 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾
∅) |
25 | | res0 4893 |
. . . . . . . . . 10
⊢ (𝑊 ↾ ∅) =
∅ |
26 | 24, 25 | eqtri 2191 |
. . . . . . . . 9
⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) =
∅ |
27 | 20, 26 | eqtri 2191 |
. . . . . . . 8
⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) =
∅ |
28 | 27 | a1i 9 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅) |
29 | 2 | elexi 2742 |
. . . . . . . . . 10
⊢ (𝐸‘ndx) ∈
V |
30 | 8 | elexd 2743 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V) |
31 | | opelxpi 4641 |
. . . . . . . . . 10
⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
32 | 29, 30, 31 | sylancr 412 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V)) |
33 | | relsng 4712 |
. . . . . . . . . 10
⊢
(〈(𝐸‘ndx), 𝐶〉 ∈ V → (Rel {〈(𝐸‘ndx), 𝐶〉} ↔ 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V))) |
34 | 10, 33 | syl 14 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (Rel {〈(𝐸‘ndx), 𝐶〉} ↔ 〈(𝐸‘ndx), 𝐶〉 ∈ (V ×
V))) |
35 | 32, 34 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {〈(𝐸‘ndx), 𝐶〉}) |
36 | | dmsnopg 5080 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑉 → dom {〈(𝐸‘ndx), 𝐶〉} = {(𝐸‘ndx)}) |
37 | 36 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → dom {〈(𝐸‘ndx), 𝐶〉} = {(𝐸‘ndx)}) |
38 | | eqimss 3201 |
. . . . . . . . 9
⊢ (dom
{〈(𝐸‘ndx), 𝐶〉} = {(𝐸‘ndx)} → dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) |
39 | 37, 38 | syl 14 |
. . . . . . . 8
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) |
40 | | relssres 4927 |
. . . . . . . 8
⊢ ((Rel
{〈(𝐸‘ndx), 𝐶〉} ∧ dom {〈(𝐸‘ndx), 𝐶〉} ⊆ {(𝐸‘ndx)}) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
41 | 35, 39, 40 | syl2anc 409 |
. . . . . . 7
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
42 | 28, 41 | uneq12d 3282 |
. . . . . 6
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({〈(𝐸‘ndx), 𝐶〉} ↾ {(𝐸‘ndx)})) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉})) |
43 | | resundir 4903 |
. . . . . 6
⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪
{〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪
({〈(𝐸‘ndx),
𝐶〉} ↾ {(𝐸‘ndx)})) |
44 | | un0 3447 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = {〈(𝐸‘ndx), 𝐶〉} |
45 | | uncom 3271 |
. . . . . . 7
⊢
({〈(𝐸‘ndx), 𝐶〉} ∪ ∅) = (∅ ∪
{〈(𝐸‘ndx), 𝐶〉}) |
46 | 44, 45 | eqtr3i 2193 |
. . . . . 6
⊢
{〈(𝐸‘ndx), 𝐶〉} = (∅ ∪ {〈(𝐸‘ndx), 𝐶〉}) |
47 | 42, 43, 46 | 3eqtr4g 2228 |
. . . . 5
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)}) = {〈(𝐸‘ndx), 𝐶〉}) |
48 | 47 | fveq1d 5496 |
. . . 4
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
49 | 19, 48 | eqtr3id 2217 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx))) |
50 | | fvsng 5690 |
. . . 4
⊢ (((𝐸‘ndx) ∈ ℕ ∧
𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
51 | 2, 8, 50 | sylancr 412 |
. . 3
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({〈(𝐸‘ndx), 𝐶〉}‘(𝐸‘ndx)) = 𝐶) |
52 | 49, 51 | eqtrd 2203 |
. 2
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), 𝐶〉})‘(𝐸‘ndx)) = 𝐶) |
53 | 5, 16, 52 | 3eqtrrd 2208 |
1
⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) |