Step | Hyp | Ref
| Expression |
1 | | cicrcl 17750 |
. 2
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β π β (BaseβπΆ)) |
2 | | ciclcl 17749 |
. 2
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β π
β (BaseβπΆ)) |
3 | | eqid 2733 |
. . . . 5
β’
(IsoβπΆ) =
(IsoβπΆ) |
4 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | simpl 484 |
. . . . 5
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β πΆ β Cat) |
6 | | simpr 486 |
. . . . . 6
β’ ((π β (BaseβπΆ) β§ π
β (BaseβπΆ)) β π
β (BaseβπΆ)) |
7 | 6 | adantl 483 |
. . . . 5
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β π
β (BaseβπΆ)) |
8 | | simpl 484 |
. . . . . 6
β’ ((π β (BaseβπΆ) β§ π
β (BaseβπΆ)) β π β (BaseβπΆ)) |
9 | 8 | adantl 483 |
. . . . 5
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β π β (BaseβπΆ)) |
10 | 3, 4, 5, 7, 9 | cic 17746 |
. . . 4
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π
( βπ βπΆ)π β βπ π β (π
(IsoβπΆ)π))) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’
(InvβπΆ) =
(InvβπΆ) |
12 | 4, 11, 5, 7, 9, 3 | isoval 17712 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π
(IsoβπΆ)π) = dom (π
(InvβπΆ)π)) |
13 | 4, 11, 5, 9, 7 | invsym2 17710 |
. . . . . . . . . . . 12
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β β‘(π(InvβπΆ)π
) = (π
(InvβπΆ)π)) |
14 | 13 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π
(InvβπΆ)π) = β‘(π(InvβπΆ)π
)) |
15 | 14 | dmeqd 5906 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β dom (π
(InvβπΆ)π) = dom β‘(π(InvβπΆ)π
)) |
16 | | df-rn 5688 |
. . . . . . . . . 10
β’ ran
(π(InvβπΆ)π
) = dom β‘(π(InvβπΆ)π
) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β dom (π
(InvβπΆ)π) = ran (π(InvβπΆ)π
)) |
18 | 12, 17 | eqtrd 2773 |
. . . . . . . 8
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π
(IsoβπΆ)π) = ran (π(InvβπΆ)π
)) |
19 | 18 | eleq2d 2820 |
. . . . . . 7
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β (π
(IsoβπΆ)π) β π β ran (π(InvβπΆ)π
))) |
20 | | vex 3479 |
. . . . . . . 8
β’ π β V |
21 | | elrng 5892 |
. . . . . . . 8
β’ (π β V β (π β ran (π(InvβπΆ)π
) β βπ π(π(InvβπΆ)π
)π)) |
22 | 20, 21 | mp1i 13 |
. . . . . . 7
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β ran (π(InvβπΆ)π
) β βπ π(π(InvβπΆ)π
)π)) |
23 | 19, 22 | bitrd 279 |
. . . . . 6
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β (π
(IsoβπΆ)π) β βπ π(π(InvβπΆ)π
)π)) |
24 | | df-br 5150 |
. . . . . . . 8
β’ (π(π(InvβπΆ)π
)π β β¨π, πβ© β (π(InvβπΆ)π
)) |
25 | 24 | exbii 1851 |
. . . . . . 7
β’
(βπ π(π(InvβπΆ)π
)π β βπβ¨π, πβ© β (π(InvβπΆ)π
)) |
26 | | vex 3479 |
. . . . . . . . . . 11
β’ π β V |
27 | 26, 20 | opeldm 5908 |
. . . . . . . . . 10
β’
(β¨π, πβ© β (π(InvβπΆ)π
) β π β dom (π(InvβπΆ)π
)) |
28 | 4, 11, 5, 9, 7, 3 | isoval 17712 |
. . . . . . . . . . . . 13
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π(IsoβπΆ)π
) = dom (π(InvβπΆ)π
)) |
29 | 28 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β dom (π(InvβπΆ)π
) = (π(IsoβπΆ)π
)) |
30 | 29 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β dom (π(InvβπΆ)π
) β π β (π(IsoβπΆ)π
))) |
31 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β§ π β (π(IsoβπΆ)π
)) β πΆ β Cat) |
32 | 9 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β§ π β (π(IsoβπΆ)π
)) β π β (BaseβπΆ)) |
33 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β§ π β (π(IsoβπΆ)π
)) β π
β (BaseβπΆ)) |
34 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β§ π β (π(IsoβπΆ)π
)) β π β (π(IsoβπΆ)π
)) |
35 | 3, 4, 31, 32, 33, 34 | brcici 17747 |
. . . . . . . . . . . 12
β’ (((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β§ π β (π(IsoβπΆ)π
)) β π( βπ βπΆ)π
) |
36 | 35 | ex 414 |
. . . . . . . . . . 11
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β (π(IsoβπΆ)π
) β π( βπ βπΆ)π
)) |
37 | 30, 36 | sylbid 239 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β dom (π(InvβπΆ)π
) β π( βπ βπΆ)π
)) |
38 | 27, 37 | syl5com 31 |
. . . . . . . . 9
β’
(β¨π, πβ© β (π(InvβπΆ)π
) β ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β π( βπ βπΆ)π
)) |
39 | 38 | exlimiv 1934 |
. . . . . . . 8
β’
(βπβ¨π, πβ© β (π(InvβπΆ)π
) β ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β π( βπ βπΆ)π
)) |
40 | 39 | com12 32 |
. . . . . . 7
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (βπβ¨π, πβ© β (π(InvβπΆ)π
) β π( βπ βπΆ)π
)) |
41 | 25, 40 | biimtrid 241 |
. . . . . 6
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (βπ π(π(InvβπΆ)π
)π β π( βπ βπΆ)π
)) |
42 | 23, 41 | sylbid 239 |
. . . . 5
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π β (π
(IsoβπΆ)π) β π( βπ βπΆ)π
)) |
43 | 42 | exlimdv 1937 |
. . . 4
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (βπ π β (π
(IsoβπΆ)π) β π( βπ βπΆ)π
)) |
44 | 10, 43 | sylbid 239 |
. . 3
β’ ((πΆ β Cat β§ (π β (BaseβπΆ) β§ π
β (BaseβπΆ))) β (π
( βπ βπΆ)π β π( βπ βπΆ)π
)) |
45 | 44 | impancom 453 |
. 2
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β ((π β (BaseβπΆ) β§ π
β (BaseβπΆ)) β π( βπ βπΆ)π
)) |
46 | 1, 2, 45 | mp2and 698 |
1
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β π( βπ βπΆ)π
) |