Step | Hyp | Ref
| Expression |
1 | | strsetsid.s |
. . . 4
⊢ (𝜑 → 𝑆 Struct 〈𝑀, 𝑁〉) |
2 | | structex 12428 |
. . . 4
⊢ (𝑆 Struct 〈𝑀, 𝑁〉 → 𝑆 ∈ V) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
4 | | strsetsid.d |
. . 3
⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆) |
5 | | strsetsid.e |
. . . . 5
⊢ 𝐸 = Slot (𝐸‘ndx) |
6 | | isstructim 12430 |
. . . . . . . . 9
⊢ (𝑆 Struct 〈𝑀, 𝑁〉 → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝑆 ∖ {∅}) ∧ dom 𝑆 ⊆ (𝑀...𝑁))) |
7 | 1, 6 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝑆 ∖ {∅}) ∧ dom 𝑆 ⊆ (𝑀...𝑁))) |
8 | 7 | simp3d 1006 |
. . . . . . 7
⊢ (𝜑 → dom 𝑆 ⊆ (𝑀...𝑁)) |
9 | 7 | simp1d 1004 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁)) |
10 | 9 | simp1d 1004 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | | fzssnn 10024 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (𝑀...𝑁) ⊆ ℕ) |
13 | 8, 12 | sstrd 3157 |
. . . . . 6
⊢ (𝜑 → dom 𝑆 ⊆ ℕ) |
14 | 13, 4 | sseldd 3148 |
. . . . 5
⊢ (𝜑 → (𝐸‘ndx) ∈ ℕ) |
15 | 5, 3, 14 | strnfvnd 12436 |
. . . 4
⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘(𝐸‘ndx))) |
16 | | strsetsid.f |
. . . . 5
⊢ (𝜑 → Fun 𝑆) |
17 | | funfvex 5513 |
. . . . 5
⊢ ((Fun
𝑆 ∧ (𝐸‘ndx) ∈ dom 𝑆) → (𝑆‘(𝐸‘ndx)) ∈ V) |
18 | 16, 4, 17 | syl2anc 409 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) ∈ V) |
19 | 15, 18 | eqeltrd 2247 |
. . 3
⊢ (𝜑 → (𝐸‘𝑆) ∈ V) |
20 | | setsvala 12447 |
. . 3
⊢ ((𝑆 ∈ V ∧ (𝐸‘ndx) ∈ dom 𝑆 ∧ (𝐸‘𝑆) ∈ V) → (𝑆 sSet 〈(𝐸‘ndx), (𝐸‘𝑆)〉) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝐸‘𝑆)〉})) |
21 | 3, 4, 19, 20 | syl3anc 1233 |
. 2
⊢ (𝜑 → (𝑆 sSet 〈(𝐸‘ndx), (𝐸‘𝑆)〉) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝐸‘𝑆)〉})) |
22 | 15 | opeq2d 3772 |
. . . 4
⊢ (𝜑 → 〈(𝐸‘ndx), (𝐸‘𝑆)〉 = 〈(𝐸‘ndx), (𝑆‘(𝐸‘ndx))〉) |
23 | 22 | sneqd 3596 |
. . 3
⊢ (𝜑 → {〈(𝐸‘ndx), (𝐸‘𝑆)〉} = {〈(𝐸‘ndx), (𝑆‘(𝐸‘ndx))〉}) |
24 | 23 | uneq2d 3281 |
. 2
⊢ (𝜑 → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝐸‘𝑆)〉}) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝑆‘(𝐸‘ndx))〉})) |
25 | | nnssz 9229 |
. . . . 5
⊢ ℕ
⊆ ℤ |
26 | 13, 25 | sstrdi 3159 |
. . . 4
⊢ (𝜑 → dom 𝑆 ⊆ ℤ) |
27 | | zdceq 9287 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
DECID 𝑥 =
𝑦) |
28 | 27 | rgen2a 2524 |
. . . 4
⊢
∀𝑥 ∈
ℤ ∀𝑦 ∈
ℤ DECID 𝑥 = 𝑦 |
29 | | ssralv 3211 |
. . . . . 6
⊢ (dom
𝑆 ⊆ ℤ →
(∀𝑦 ∈ ℤ
DECID 𝑥 =
𝑦 → ∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦)) |
30 | 29 | ralimdv 2538 |
. . . . 5
⊢ (dom
𝑆 ⊆ ℤ →
(∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
DECID 𝑥 =
𝑦 → ∀𝑥 ∈ ℤ ∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦)) |
31 | | ssralv 3211 |
. . . . 5
⊢ (dom
𝑆 ⊆ ℤ →
(∀𝑥 ∈ ℤ
∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦)) |
32 | 30, 31 | syld 45 |
. . . 4
⊢ (dom
𝑆 ⊆ ℤ →
(∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
DECID 𝑥 =
𝑦 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦)) |
33 | 26, 28, 32 | mpisyl 1439 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦) |
34 | | funresdfunsndc 6485 |
. . 3
⊢
((∀𝑥 ∈
dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦 ∧ Fun 𝑆 ∧ (𝐸‘ndx) ∈ dom 𝑆) → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝑆‘(𝐸‘ndx))〉}) = 𝑆) |
35 | 33, 16, 4, 34 | syl3anc 1233 |
. 2
⊢ (𝜑 → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {〈(𝐸‘ndx), (𝑆‘(𝐸‘ndx))〉}) = 𝑆) |
36 | 21, 24, 35 | 3eqtrrd 2208 |
1
⊢ (𝜑 → 𝑆 = (𝑆 sSet 〈(𝐸‘ndx), (𝐸‘𝑆)〉)) |