Step | Hyp | Ref
| Expression |
1 | | setsid.e |
. . . 4
β’ πΈ = Slot (πΈβndx) |
2 | | id 22 |
. . . 4
β’ (π β V β π β V) |
3 | 1, 2 | strfvnd 17062 |
. . 3
β’ (π β V β (πΈβπ) = (πβ(πΈβndx))) |
4 | | ovex 7391 |
. . . . 5
β’ (π sSet β¨π·, πΆβ©) β V |
5 | 4, 1 | strfvn 17063 |
. . . 4
β’ (πΈβ(π sSet β¨π·, πΆβ©)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx)) |
6 | | setsres 17055 |
. . . . . 6
β’ (π β V β ((π sSet β¨π·, πΆβ©) βΎ (V β {π·})) = (π βΎ (V β {π·}))) |
7 | 6 | fveq1d 6845 |
. . . . 5
β’ (π β V β (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π βΎ (V β {π·}))β(πΈβndx))) |
8 | | fvex 6856 |
. . . . . . 7
β’ (πΈβndx) β
V |
9 | | setsnid.n |
. . . . . . 7
β’ (πΈβndx) β π· |
10 | | eldifsn 4748 |
. . . . . . 7
β’ ((πΈβndx) β (V β
{π·}) β ((πΈβndx) β V β§
(πΈβndx) β π·)) |
11 | 8, 9, 10 | mpbir2an 710 |
. . . . . 6
β’ (πΈβndx) β (V β
{π·}) |
12 | | fvres 6862 |
. . . . . 6
β’ ((πΈβndx) β (V β
{π·}) β (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx))) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
β’ (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx)) |
14 | | fvres 6862 |
. . . . . 6
β’ ((πΈβndx) β (V β
{π·}) β ((π βΎ (V β {π·}))β(πΈβndx)) = (πβ(πΈβndx))) |
15 | 11, 14 | ax-mp 5 |
. . . . 5
β’ ((π βΎ (V β {π·}))β(πΈβndx)) = (πβ(πΈβndx)) |
16 | 7, 13, 15 | 3eqtr3g 2796 |
. . . 4
β’ (π β V β ((π sSet β¨π·, πΆβ©)β(πΈβndx)) = (πβ(πΈβndx))) |
17 | 5, 16 | eqtrid 2785 |
. . 3
β’ (π β V β (πΈβ(π sSet β¨π·, πΆβ©)) = (πβ(πΈβndx))) |
18 | 3, 17 | eqtr4d 2776 |
. 2
β’ (π β V β (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©))) |
19 | 1 | str0 17066 |
. . 3
β’ β
=
(πΈββ
) |
20 | | fvprc 6835 |
. . 3
β’ (Β¬
π β V β (πΈβπ) = β
) |
21 | | reldmsets 17042 |
. . . . 5
β’ Rel dom
sSet |
22 | 21 | ovprc1 7397 |
. . . 4
β’ (Β¬
π β V β (π sSet β¨π·, πΆβ©) = β
) |
23 | 22 | fveq2d 6847 |
. . 3
β’ (Β¬
π β V β (πΈβ(π sSet β¨π·, πΆβ©)) = (πΈββ
)) |
24 | 19, 20, 23 | 3eqtr4a 2799 |
. 2
β’ (Β¬
π β V β (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©))) |
25 | 18, 24 | pm2.61i 182 |
1
β’ (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©)) |