Step | Hyp | Ref
| Expression |
1 | | invfval.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
2 | | invfval.n |
. . . 4
β’ π = (InvβπΆ) |
3 | | invfval.c |
. . . 4
β’ (π β πΆ β Cat) |
4 | | invfval.x |
. . . 4
β’ (π β π β π΅) |
5 | | invfval.y |
. . . 4
β’ (π β π β π΅) |
6 | | eqid 2730 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
7 | 1, 2, 3, 4, 5, 6 | invss 17712 |
. . 3
β’ (π β (πππ) β ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π))) |
8 | | relxp 5693 |
. . 3
β’ Rel
((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) |
9 | | relss 5780 |
. . 3
β’ ((πππ) β ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) β (Rel ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) β Rel (πππ))) |
10 | 7, 8, 9 | mpisyl 21 |
. 2
β’ (π β Rel (πππ)) |
11 | | eqid 2730 |
. . . . . 6
β’
(SectβπΆ) =
(SectβπΆ) |
12 | 3 | adantr 479 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β πΆ β Cat) |
13 | 5 | adantr 479 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π β π΅) |
14 | 4 | adantr 479 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π β π΅) |
15 | 1, 2, 3, 4, 5, 11 | isinv 17711 |
. . . . . . . 8
β’ (π β (π(πππ)π β (π(π(SectβπΆ)π)π β§ π(π(SectβπΆ)π)π))) |
16 | 15 | simplbda 498 |
. . . . . . 7
β’ ((π β§ π(πππ)π) β π(π(SectβπΆ)π)π) |
17 | 16 | adantrr 713 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π(π(SectβπΆ)π)π) |
18 | 1, 2, 3, 4, 5, 11 | isinv 17711 |
. . . . . . . 8
β’ (π β (π(πππ)β β (π(π(SectβπΆ)π)β β§ β(π(SectβπΆ)π)π))) |
19 | 18 | simprbda 497 |
. . . . . . 7
β’ ((π β§ π(πππ)β) β π(π(SectβπΆ)π)β) |
20 | 19 | adantrl 712 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π(π(SectβπΆ)π)β) |
21 | 1, 11, 12, 13, 14, 17, 20 | sectcan 17706 |
. . . . 5
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π = β) |
22 | 21 | ex 411 |
. . . 4
β’ (π β ((π(πππ)π β§ π(πππ)β) β π = β)) |
23 | 22 | alrimiv 1928 |
. . 3
β’ (π β ββ((π(πππ)π β§ π(πππ)β) β π = β)) |
24 | 23 | alrimivv 1929 |
. 2
β’ (π β βπβπββ((π(πππ)π β§ π(πππ)β) β π = β)) |
25 | | dffun2 6552 |
. 2
β’ (Fun
(πππ) β (Rel (πππ) β§ βπβπββ((π(πππ)π β§ π(πππ)β) β π = β))) |
26 | 10, 24, 25 | sylanbrc 581 |
1
β’ (π β Fun (πππ)) |