Step | Hyp | Ref
| Expression |
1 | | setsslid.e |
. . . . 5
β’ (πΈ = Slot (πΈβndx) β§ (πΈβndx) β β) |
2 | 1 | simpri 113 |
. . . 4
β’ (πΈβndx) β
β |
3 | | setsvala 12493 |
. . . 4
β’ ((π β π΄ β§ (πΈβndx) β β β§ πΆ β π) β (π sSet β¨(πΈβndx), πΆβ©) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})) |
4 | 2, 3 | mp3an2 1325 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β (π sSet β¨(πΈβndx), πΆβ©) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})) |
5 | 4 | fveq2d 5520 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (πΈβ(π sSet β¨(πΈβndx), πΆβ©)) = (πΈβ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}))) |
6 | 1 | simpli 111 |
. . 3
β’ πΈ = Slot (πΈβndx) |
7 | | resexg 4948 |
. . . 4
β’ (π β π΄ β (π βΎ (V β {(πΈβndx)})) β V) |
8 | | simpr 110 |
. . . . . 6
β’ ((π β π΄ β§ πΆ β π) β πΆ β π) |
9 | | opexg 4229 |
. . . . . 6
β’ (((πΈβndx) β β β§
πΆ β π) β β¨(πΈβndx), πΆβ© β V) |
10 | 2, 8, 9 | sylancr 414 |
. . . . 5
β’ ((π β π΄ β§ πΆ β π) β β¨(πΈβndx), πΆβ© β V) |
11 | | snexg 4185 |
. . . . 5
β’
(β¨(πΈβndx), πΆβ© β V β {β¨(πΈβndx), πΆβ©} β V) |
12 | 10, 11 | syl 14 |
. . . 4
β’ ((π β π΄ β§ πΆ β π) β {β¨(πΈβndx), πΆβ©} β V) |
13 | | unexg 4444 |
. . . 4
β’ (((π βΎ (V β {(πΈβndx)})) β V β§
{β¨(πΈβndx), πΆβ©} β V) β ((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) β
V) |
14 | 7, 12, 13 | syl2an2r 595 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) β V) |
15 | 2 | a1i 9 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β (πΈβndx) β β) |
16 | 6, 14, 15 | strnfvnd 12482 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (πΈβ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})) = (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx))) |
17 | | snidg 3622 |
. . . . 5
β’ ((πΈβndx) β β
β (πΈβndx) β
{(πΈβndx)}) |
18 | | fvres 5540 |
. . . . 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 4920 |
. . . . . . . . 9
β’ ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) = (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) |
21 | | incom 3328 |
. . . . . . . . . . . 12
β’ ((V
β {(πΈβndx)})
β© {(πΈβndx)}) =
({(πΈβndx)} β© (V
β {(πΈβndx)})) |
22 | | disjdif 3496 |
. . . . . . . . . . . 12
β’ ({(πΈβndx)} β© (V β
{(πΈβndx)})) =
β
|
23 | 21, 22 | eqtri 2198 |
. . . . . . . . . . 11
β’ ((V
β {(πΈβndx)})
β© {(πΈβndx)}) =
β
|
24 | 23 | reseq2i 4905 |
. . . . . . . . . 10
β’ (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) = (π βΎ
β
) |
25 | | res0 4912 |
. . . . . . . . . 10
β’ (π βΎ β
) =
β
|
26 | 24, 25 | eqtri 2198 |
. . . . . . . . 9
β’ (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) =
β
|
27 | 20, 26 | eqtri 2198 |
. . . . . . . 8
β’ ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) =
β
|
28 | 27 | a1i 9 |
. . . . . . 7
β’ ((π β π΄ β§ πΆ β π) β ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) = β
) |
29 | 2 | elexi 2750 |
. . . . . . . . . 10
β’ (πΈβndx) β
V |
30 | 8 | elexd 2751 |
. . . . . . . . . 10
β’ ((π β π΄ β§ πΆ β π) β πΆ β V) |
31 | | opelxpi 4659 |
. . . . . . . . . 10
β’ (((πΈβndx) β V β§ πΆ β V) β β¨(πΈβndx), πΆβ© β (V Γ
V)) |
32 | 29, 30, 31 | sylancr 414 |
. . . . . . . . 9
β’ ((π β π΄ β§ πΆ β π) β β¨(πΈβndx), πΆβ© β (V Γ
V)) |
33 | | relsng 4730 |
. . . . . . . . . 10
β’
(β¨(πΈβndx), πΆβ© β V β (Rel {β¨(πΈβndx), πΆβ©} β β¨(πΈβndx), πΆβ© β (V Γ
V))) |
34 | 10, 33 | syl 14 |
. . . . . . . . 9
β’ ((π β π΄ β§ πΆ β π) β (Rel {β¨(πΈβndx), πΆβ©} β β¨(πΈβndx), πΆβ© β (V Γ
V))) |
35 | 32, 34 | mpbird 167 |
. . . . . . . 8
β’ ((π β π΄ β§ πΆ β π) β Rel {β¨(πΈβndx), πΆβ©}) |
36 | | dmsnopg 5101 |
. . . . . . . . . 10
β’ (πΆ β π β dom {β¨(πΈβndx), πΆβ©} = {(πΈβndx)}) |
37 | 36 | adantl 277 |
. . . . . . . . 9
β’ ((π β π΄ β§ πΆ β π) β dom {β¨(πΈβndx), πΆβ©} = {(πΈβndx)}) |
38 | | eqimss 3210 |
. . . . . . . . 9
β’ (dom
{β¨(πΈβndx), πΆβ©} = {(πΈβndx)} β dom {β¨(πΈβndx), πΆβ©} β {(πΈβndx)}) |
39 | 37, 38 | syl 14 |
. . . . . . . 8
β’ ((π β π΄ β§ πΆ β π) β dom {β¨(πΈβndx), πΆβ©} β {(πΈβndx)}) |
40 | | relssres 4946 |
. . . . . . . 8
β’ ((Rel
{β¨(πΈβndx), πΆβ©} β§ dom {β¨(πΈβndx), πΆβ©} β {(πΈβndx)}) β ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
41 | 35, 39, 40 | syl2anc 411 |
. . . . . . 7
β’ ((π β π΄ β§ πΆ β π) β ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
42 | 28, 41 | uneq12d 3291 |
. . . . . 6
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) βͺ ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)})) = (β
βͺ
{β¨(πΈβndx), πΆβ©})) |
43 | | resundir 4922 |
. . . . . 6
β’ (((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)}) = (((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) βͺ
({β¨(πΈβndx),
πΆβ©} βΎ {(πΈβndx)})) |
44 | | un0 3457 |
. . . . . . 7
β’
({β¨(πΈβndx), πΆβ©} βͺ β
) = {β¨(πΈβndx), πΆβ©} |
45 | | uncom 3280 |
. . . . . . 7
β’
({β¨(πΈβndx), πΆβ©} βͺ β
) = (β
βͺ
{β¨(πΈβndx), πΆβ©}) |
46 | 44, 45 | eqtr3i 2200 |
. . . . . 6
β’
{β¨(πΈβndx), πΆβ©} = (β
βͺ {β¨(πΈβndx), πΆβ©}) |
47 | 42, 43, 46 | 3eqtr4g 2235 |
. . . . 5
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
48 | 47 | fveq1d 5518 |
. . . 4
β’ ((π β π΄ β§ πΆ β π) β ((((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)})β(πΈβndx)) = ({β¨(πΈβndx), πΆβ©}β(πΈβndx))) |
49 | 19, 48 | eqtr3id 2224 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx)) = ({β¨(πΈβndx), πΆβ©}β(πΈβndx))) |
50 | | fvsng 5713 |
. . . 4
β’ (((πΈβndx) β β β§
πΆ β π) β ({β¨(πΈβndx), πΆβ©}β(πΈβndx)) = πΆ) |
51 | 2, 8, 50 | sylancr 414 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β ({β¨(πΈβndx), πΆβ©}β(πΈβndx)) = πΆ) |
52 | 49, 51 | eqtrd 2210 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx)) = πΆ) |
53 | 5, 16, 52 | 3eqtrrd 2215 |
1
β’ ((π β π΄ β§ πΆ β π) β πΆ = (πΈβ(π sSet β¨(πΈβndx), πΆβ©))) |