Step | Hyp | Ref
| Expression |
1 | | ressval3d.u |
. 2
β’ (π β π΄ β π΅) |
2 | | sspss 4060 |
. . . 4
β’ (π΄ β π΅ β (π΄ β π΅ β¨ π΄ = π΅)) |
3 | | dfpss3 4047 |
. . . . 5
β’ (π΄ β π΅ β (π΄ β π΅ β§ Β¬ π΅ β π΄)) |
4 | 3 | orbi1i 913 |
. . . 4
β’ ((π΄ β π΅ β¨ π΄ = π΅) β ((π΄ β π΅ β§ Β¬ π΅ β π΄) β¨ π΄ = π΅)) |
5 | 2, 4 | bitri 275 |
. . 3
β’ (π΄ β π΅ β ((π΄ β π΅ β§ Β¬ π΅ β π΄) β¨ π΄ = π΅)) |
6 | | simplr 768 |
. . . . . . 7
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β Β¬ π΅ β π΄) |
7 | | ressval3d.s |
. . . . . . . 8
β’ (π β π β π) |
8 | 7 | adantl 483 |
. . . . . . 7
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β π β π) |
9 | | simpl 484 |
. . . . . . . 8
β’ ((π΄ β π΅ β§ Β¬ π΅ β π΄) β π΄ β π΅) |
10 | | ressval3d.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
11 | 10 | fvexi 6857 |
. . . . . . . . 9
β’ π΅ β V |
12 | 11 | a1i 11 |
. . . . . . . 8
β’ (π β π΅ β V) |
13 | | ssexg 5281 |
. . . . . . . 8
β’ ((π΄ β π΅ β§ π΅ β V) β π΄ β V) |
14 | 9, 12, 13 | syl2an 597 |
. . . . . . 7
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β π΄ β V) |
15 | | ressval3d.r |
. . . . . . . 8
β’ π
= (π βΎs π΄) |
16 | 15, 10 | ressval2 17122 |
. . . . . . 7
β’ ((Β¬
π΅ β π΄ β§ π β π β§ π΄ β V) β π
= (π sSet β¨(Baseβndx), (π΄ β© π΅)β©)) |
17 | 6, 8, 14, 16 | syl3anc 1372 |
. . . . . 6
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β π
= (π sSet β¨(Baseβndx), (π΄ β© π΅)β©)) |
18 | | ressval3d.e |
. . . . . . . . . 10
β’ πΈ =
(Baseβndx) |
19 | 18 | a1i 11 |
. . . . . . . . 9
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β πΈ = (Baseβndx)) |
20 | | df-ss 3928 |
. . . . . . . . . . . . 13
β’ (π΄ β π΅ β (π΄ β© π΅) = π΄) |
21 | 20 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π΄ β π΅ β (π΄ β© π΅) = π΄) |
22 | 21 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π΄ β π΅ β π΄ = (π΄ β© π΅)) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β π΅ β§ Β¬ π΅ β π΄) β π΄ = (π΄ β© π΅)) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β π΄ = (π΄ β© π΅)) |
25 | 19, 24 | opeq12d 4839 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β β¨πΈ, π΄β© = β¨(Baseβndx), (π΄ β© π΅)β©) |
26 | 25 | eqcomd 2739 |
. . . . . . 7
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β β¨(Baseβndx), (π΄ β© π΅)β© = β¨πΈ, π΄β©) |
27 | 26 | oveq2d 7374 |
. . . . . 6
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β (π sSet β¨(Baseβndx), (π΄ β© π΅)β©) = (π sSet β¨πΈ, π΄β©)) |
28 | 17, 27 | eqtrd 2773 |
. . . . 5
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β§ π) β π
= (π sSet β¨πΈ, π΄β©)) |
29 | 28 | ex 414 |
. . . 4
β’ ((π΄ β π΅ β§ Β¬ π΅ β π΄) β (π β π
= (π sSet β¨πΈ, π΄β©))) |
30 | 15 | a1i 11 |
. . . . . . 7
β’ ((π΄ = π΅ β§ π) β π
= (π βΎs π΄)) |
31 | | oveq2 7366 |
. . . . . . . 8
β’ (π΄ = π΅ β (π βΎs π΄) = (π βΎs π΅)) |
32 | 31 | adantr 482 |
. . . . . . 7
β’ ((π΄ = π΅ β§ π) β (π βΎs π΄) = (π βΎs π΅)) |
33 | 7 | adantl 483 |
. . . . . . . 8
β’ ((π΄ = π΅ β§ π) β π β π) |
34 | 10 | ressid 17130 |
. . . . . . . 8
β’ (π β π β (π βΎs π΅) = π) |
35 | 33, 34 | syl 17 |
. . . . . . 7
β’ ((π΄ = π΅ β§ π) β (π βΎs π΅) = π) |
36 | 30, 32, 35 | 3eqtrd 2777 |
. . . . . 6
β’ ((π΄ = π΅ β§ π) β π
= π) |
37 | | baseid 17091 |
. . . . . . . 8
β’ Base =
Slot (Baseβndx) |
38 | | ressval3d.f |
. . . . . . . 8
β’ (π β Fun π) |
39 | | ressval3d.d |
. . . . . . . . 9
β’ (π β πΈ β dom π) |
40 | 18, 39 | eqeltrrid 2839 |
. . . . . . . 8
β’ (π β (Baseβndx) β
dom π) |
41 | 37, 7, 38, 40 | setsidvald 17076 |
. . . . . . 7
β’ (π β π = (π sSet β¨(Baseβndx),
(Baseβπ)β©)) |
42 | 41 | adantl 483 |
. . . . . 6
β’ ((π΄ = π΅ β§ π) β π = (π sSet β¨(Baseβndx),
(Baseβπ)β©)) |
43 | 18 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ = π΅ β§ π) β πΈ = (Baseβndx)) |
44 | | simpl 484 |
. . . . . . . . . 10
β’ ((π΄ = π΅ β§ π) β π΄ = π΅) |
45 | 44, 10 | eqtrdi 2789 |
. . . . . . . . 9
β’ ((π΄ = π΅ β§ π) β π΄ = (Baseβπ)) |
46 | 43, 45 | opeq12d 4839 |
. . . . . . . 8
β’ ((π΄ = π΅ β§ π) β β¨πΈ, π΄β© = β¨(Baseβndx),
(Baseβπ)β©) |
47 | 46 | eqcomd 2739 |
. . . . . . 7
β’ ((π΄ = π΅ β§ π) β β¨(Baseβndx),
(Baseβπ)β© =
β¨πΈ, π΄β©) |
48 | 47 | oveq2d 7374 |
. . . . . 6
β’ ((π΄ = π΅ β§ π) β (π sSet β¨(Baseβndx),
(Baseβπ)β©) =
(π sSet β¨πΈ, π΄β©)) |
49 | 36, 42, 48 | 3eqtrd 2777 |
. . . . 5
β’ ((π΄ = π΅ β§ π) β π
= (π sSet β¨πΈ, π΄β©)) |
50 | 49 | ex 414 |
. . . 4
β’ (π΄ = π΅ β (π β π
= (π sSet β¨πΈ, π΄β©))) |
51 | 29, 50 | jaoi 856 |
. . 3
β’ (((π΄ β π΅ β§ Β¬ π΅ β π΄) β¨ π΄ = π΅) β (π β π
= (π sSet β¨πΈ, π΄β©))) |
52 | 5, 51 | sylbi 216 |
. 2
β’ (π΄ β π΅ β (π β π
= (π sSet β¨πΈ, π΄β©))) |
53 | 1, 52 | mpcom 38 |
1
β’ (π β π
= (π sSet β¨πΈ, π΄β©)) |