Step | Hyp | Ref
| Expression |
1 | | strsetsid.s |
. . . 4
β’ (π β π Struct β¨π, πβ©) |
2 | | structex 12476 |
. . . 4
β’ (π Struct β¨π, πβ© β π β V) |
3 | 1, 2 | syl 14 |
. . 3
β’ (π β π β V) |
4 | | strsetsid.d |
. . 3
β’ (π β (πΈβndx) β dom π) |
5 | | strsetsid.e |
. . . . 5
β’ πΈ = Slot (πΈβndx) |
6 | | isstructim 12478 |
. . . . . . . . 9
β’ (π Struct β¨π, πβ© β ((π β β β§ π β β β§ π β€ π) β§ Fun (π β {β
}) β§ dom π β (π...π))) |
7 | 1, 6 | syl 14 |
. . . . . . . 8
β’ (π β ((π β β β§ π β β β§ π β€ π) β§ Fun (π β {β
}) β§ dom π β (π...π))) |
8 | 7 | simp3d 1011 |
. . . . . . 7
β’ (π β dom π β (π...π)) |
9 | 7 | simp1d 1009 |
. . . . . . . . 9
β’ (π β (π β β β§ π β β β§ π β€ π)) |
10 | 9 | simp1d 1009 |
. . . . . . . 8
β’ (π β π β β) |
11 | | fzssnn 10070 |
. . . . . . . 8
β’ (π β β β (π...π) β β) |
12 | 10, 11 | syl 14 |
. . . . . . 7
β’ (π β (π...π) β β) |
13 | 8, 12 | sstrd 3167 |
. . . . . 6
β’ (π β dom π β β) |
14 | 13, 4 | sseldd 3158 |
. . . . 5
β’ (π β (πΈβndx) β β) |
15 | 5, 3, 14 | strnfvnd 12484 |
. . . 4
β’ (π β (πΈβπ) = (πβ(πΈβndx))) |
16 | | strsetsid.f |
. . . . 5
β’ (π β Fun π) |
17 | | funfvex 5534 |
. . . . 5
β’ ((Fun
π β§ (πΈβndx) β dom π) β (πβ(πΈβndx)) β V) |
18 | 16, 4, 17 | syl2anc 411 |
. . . 4
β’ (π β (πβ(πΈβndx)) β V) |
19 | 15, 18 | eqeltrd 2254 |
. . 3
β’ (π β (πΈβπ) β V) |
20 | | setsvala 12495 |
. . 3
β’ ((π β V β§ (πΈβndx) β dom π β§ (πΈβπ) β V) β (π sSet β¨(πΈβndx), (πΈβπ)β©) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πΈβπ)β©})) |
21 | 3, 4, 19, 20 | syl3anc 1238 |
. 2
β’ (π β (π sSet β¨(πΈβndx), (πΈβπ)β©) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πΈβπ)β©})) |
22 | 15 | opeq2d 3787 |
. . . 4
β’ (π β β¨(πΈβndx), (πΈβπ)β© = β¨(πΈβndx), (πβ(πΈβndx))β©) |
23 | 22 | sneqd 3607 |
. . 3
β’ (π β {β¨(πΈβndx), (πΈβπ)β©} = {β¨(πΈβndx), (πβ(πΈβndx))β©}) |
24 | 23 | uneq2d 3291 |
. 2
β’ (π β ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πΈβπ)β©}) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πβ(πΈβndx))β©})) |
25 | | nnssz 9272 |
. . . . 5
β’ β
β β€ |
26 | 13, 25 | sstrdi 3169 |
. . . 4
β’ (π β dom π β β€) |
27 | | zdceq 9330 |
. . . . 5
β’ ((π₯ β β€ β§ π¦ β β€) β
DECID π₯ =
π¦) |
28 | 27 | rgen2a 2531 |
. . . 4
β’
βπ₯ β
β€ βπ¦ β
β€ DECID π₯ = π¦ |
29 | | ssralv 3221 |
. . . . . 6
β’ (dom
π β β€ β
(βπ¦ β β€
DECID π₯ =
π¦ β βπ¦ β dom πDECID π₯ = π¦)) |
30 | 29 | ralimdv 2545 |
. . . . 5
β’ (dom
π β β€ β
(βπ₯ β β€
βπ¦ β β€
DECID π₯ =
π¦ β βπ₯ β β€ βπ¦ β dom πDECID π₯ = π¦)) |
31 | | ssralv 3221 |
. . . . 5
β’ (dom
π β β€ β
(βπ₯ β β€
βπ¦ β dom πDECID π₯ = π¦ β βπ₯ β dom πβπ¦ β dom πDECID π₯ = π¦)) |
32 | 30, 31 | syld 45 |
. . . 4
β’ (dom
π β β€ β
(βπ₯ β β€
βπ¦ β β€
DECID π₯ =
π¦ β βπ₯ β dom πβπ¦ β dom πDECID π₯ = π¦)) |
33 | 26, 28, 32 | mpisyl 1446 |
. . 3
β’ (π β βπ₯ β dom πβπ¦ β dom πDECID π₯ = π¦) |
34 | | funresdfunsndc 6509 |
. . 3
β’
((βπ₯ β
dom πβπ¦ β dom πDECID π₯ = π¦ β§ Fun π β§ (πΈβndx) β dom π) β ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πβ(πΈβndx))β©}) = π) |
35 | 33, 16, 4, 34 | syl3anc 1238 |
. 2
β’ (π β ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), (πβ(πΈβndx))β©}) = π) |
36 | 21, 24, 35 | 3eqtrrd 2215 |
1
β’ (π β π = (π sSet β¨(πΈβndx), (πΈβπ)β©)) |