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 2733 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
7 | 1, 2, 3, 4, 5, 6 | invss 17708 |
. . 3
β’ (π β (πππ) β ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π))) |
8 | | relxp 5695 |
. . 3
β’ Rel
((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) |
9 | | relss 5782 |
. . 3
β’ ((πππ) β ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) β (Rel ((π(Hom βπΆ)π) Γ (π(Hom βπΆ)π)) β Rel (πππ))) |
10 | 7, 8, 9 | mpisyl 21 |
. 2
β’ (π β Rel (πππ)) |
11 | | eqid 2733 |
. . . . . 6
β’
(SectβπΆ) =
(SectβπΆ) |
12 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β πΆ β Cat) |
13 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π β π΅) |
14 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π β π΅) |
15 | 1, 2, 3, 4, 5, 11 | isinv 17707 |
. . . . . . . 8
β’ (π β (π(πππ)π β (π(π(SectβπΆ)π)π β§ π(π(SectβπΆ)π)π))) |
16 | 15 | simplbda 501 |
. . . . . . 7
β’ ((π β§ π(πππ)π) β π(π(SectβπΆ)π)π) |
17 | 16 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π(π(SectβπΆ)π)π) |
18 | 1, 2, 3, 4, 5, 11 | isinv 17707 |
. . . . . . . 8
β’ (π β (π(πππ)β β (π(π(SectβπΆ)π)β β§ β(π(SectβπΆ)π)π))) |
19 | 18 | simprbda 500 |
. . . . . . 7
β’ ((π β§ π(πππ)β) β π(π(SectβπΆ)π)β) |
20 | 19 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π(π(SectβπΆ)π)β) |
21 | 1, 11, 12, 13, 14, 17, 20 | sectcan 17702 |
. . . . 5
β’ ((π β§ (π(πππ)π β§ π(πππ)β)) β π = β) |
22 | 21 | ex 414 |
. . . 4
β’ (π β ((π(πππ)π β§ π(πππ)β) β π = β)) |
23 | 22 | alrimiv 1931 |
. . 3
β’ (π β ββ((π(πππ)π β§ π(πππ)β) β π = β)) |
24 | 23 | alrimivv 1932 |
. 2
β’ (π β βπβπββ((π(πππ)π β§ π(πππ)β) β π = β)) |
25 | | dffun2 6554 |
. 2
β’ (Fun
(πππ) β (Rel (πππ) β§ βπβπββ((π(πππ)π β§ π(πππ)β) β π = β))) |
26 | 10, 24, 25 | sylanbrc 584 |
1
β’ (π β Fun (πππ)) |