Step | Hyp | Ref
| Expression |
1 | | ciclcl 17728 |
. . . . . 6
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β π
β (BaseβπΆ)) |
2 | | cicrcl 17729 |
. . . . . 6
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β π β (BaseβπΆ)) |
3 | 1, 2 | jca 512 |
. . . . 5
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π) β (π
β (BaseβπΆ) β§ π β (BaseβπΆ))) |
4 | 3 | ex 413 |
. . . 4
β’ (πΆ β Cat β (π
( βπ
βπΆ)π β (π
β (BaseβπΆ) β§ π β (BaseβπΆ)))) |
5 | | cicrcl 17729 |
. . . . 5
β’ ((πΆ β Cat β§ π( βπ
βπΆ)π) β π β (BaseβπΆ)) |
6 | 5 | ex 413 |
. . . 4
β’ (πΆ β Cat β (π( βπ
βπΆ)π β π β (BaseβπΆ))) |
7 | 4, 6 | anim12d 609 |
. . 3
β’ (πΆ β Cat β ((π
( βπ
βπΆ)π β§ π( βπ βπΆ)π) β ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) |
8 | 7 | 3impib 1116 |
. 2
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π β§ π( βπ βπΆ)π) β ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) |
9 | | eqid 2731 |
. . . . . . . 8
β’
(IsoβπΆ) =
(IsoβπΆ) |
10 | | eqid 2731 |
. . . . . . . 8
β’
(BaseβπΆ) =
(BaseβπΆ) |
11 | | simpl 483 |
. . . . . . . 8
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β πΆ β Cat) |
12 | | simpll 765 |
. . . . . . . . 9
β’ (((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π
β (BaseβπΆ)) |
13 | 12 | adantl 482 |
. . . . . . . 8
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
β (BaseβπΆ)) |
14 | | simplr 767 |
. . . . . . . . 9
β’ (((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
15 | 14 | adantl 482 |
. . . . . . . 8
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π β (BaseβπΆ)) |
16 | 9, 10, 11, 13, 15 | cic 17725 |
. . . . . . 7
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β (π
( βπ βπΆ)π β βπ π β (π
(IsoβπΆ)π))) |
17 | | simprr 771 |
. . . . . . . 8
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π β (BaseβπΆ)) |
18 | 9, 10, 11, 15, 17 | cic 17725 |
. . . . . . 7
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β (π( βπ βπΆ)π β βπ π β (π(IsoβπΆ)π))) |
19 | 16, 18 | anbi12d 631 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β ((π
( βπ βπΆ)π β§ π( βπ βπΆ)π) β (βπ π β (π
(IsoβπΆ)π) β§ βπ π β (π(IsoβπΆ)π)))) |
20 | 11 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β πΆ β Cat) |
21 | 13 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π
β (BaseβπΆ)) |
22 | 17 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π β (BaseβπΆ)) |
23 | | eqid 2731 |
. . . . . . . . . . . . . . 15
β’
(compβπΆ) =
(compβπΆ) |
24 | 15 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π β (BaseβπΆ)) |
25 | | simplr 767 |
. . . . . . . . . . . . . . 15
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π β (π
(IsoβπΆ)π)) |
26 | | simpll 765 |
. . . . . . . . . . . . . . 15
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π β (π(IsoβπΆ)π)) |
27 | 10, 23, 9, 20, 21, 24, 22, 25, 26 | isoco 17703 |
. . . . . . . . . . . . . 14
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β (π(β¨π
, πβ©(compβπΆ)π)π) β (π
(IsoβπΆ)π)) |
28 | 9, 10, 20, 21, 22, 27 | brcici 17726 |
. . . . . . . . . . . . 13
β’ (((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β§ (πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)))) β π
( βπ βπΆ)π) |
29 | 28 | ex 413 |
. . . . . . . . . . . 12
β’ ((π β (π(IsoβπΆ)π) β§ π β (π
(IsoβπΆ)π)) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π)) |
30 | 29 | ex 413 |
. . . . . . . . . . 11
β’ (π β (π(IsoβπΆ)π) β (π β (π
(IsoβπΆ)π) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π))) |
31 | 30 | exlimiv 1933 |
. . . . . . . . . 10
β’
(βπ π β (π(IsoβπΆ)π) β (π β (π
(IsoβπΆ)π) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π))) |
32 | 31 | com12 32 |
. . . . . . . . 9
β’ (π β (π
(IsoβπΆ)π) β (βπ π β (π(IsoβπΆ)π) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π))) |
33 | 32 | exlimiv 1933 |
. . . . . . . 8
β’
(βπ π β (π
(IsoβπΆ)π) β (βπ π β (π(IsoβπΆ)π) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π))) |
34 | 33 | imp 407 |
. . . . . . 7
β’
((βπ π β (π
(IsoβπΆ)π) β§ βπ π β (π(IsoβπΆ)π)) β ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β π
( βπ βπΆ)π)) |
35 | 34 | com12 32 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β ((βπ π β (π
(IsoβπΆ)π) β§ βπ π β (π(IsoβπΆ)π)) β π
( βπ βπΆ)π)) |
36 | 19, 35 | sylbid 239 |
. . . . 5
β’ ((πΆ β Cat β§ ((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ))) β ((π
( βπ βπΆ)π β§ π( βπ βπΆ)π) β π
( βπ βπΆ)π)) |
37 | 36 | ex 413 |
. . . 4
β’ (πΆ β Cat β (((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β ((π
( βπ βπΆ)π β§ π( βπ βπΆ)π) β π
( βπ βπΆ)π))) |
38 | 37 | com23 86 |
. . 3
β’ (πΆ β Cat β ((π
( βπ
βπΆ)π β§ π( βπ βπΆ)π) β (((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π
( βπ βπΆ)π))) |
39 | 38 | 3impib 1116 |
. 2
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π β§ π( βπ βπΆ)π) β (((π
β (BaseβπΆ) β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π
( βπ βπΆ)π)) |
40 | 8, 39 | mpd 15 |
1
β’ ((πΆ β Cat β§ π
( βπ
βπΆ)π β§ π( βπ βπΆ)π) β π
( βπ βπΆ)π) |