Step | Hyp | Ref
| Expression |
1 | | initoeu1.a |
. . 3
β’ (π β π΄ β (InitOβπΆ)) |
2 | | eqid 2737 |
. . . 4
β’
(BaseβπΆ) =
(BaseβπΆ) |
3 | | eqid 2737 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
4 | | initoeu1.c |
. . . 4
β’ (π β πΆ β Cat) |
5 | 2, 3, 4 | isinitoi 17892 |
. . 3
β’ ((π β§ π΄ β (InitOβπΆ)) β (π΄ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π))) |
6 | 1, 5 | mpdan 686 |
. 2
β’ (π β (π΄ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π))) |
7 | | initoeu1.b |
. . . . 5
β’ (π β π΅ β (InitOβπΆ)) |
8 | 2, 3, 4 | isinitoi 17892 |
. . . . 5
β’ ((π β§ π΅ β (InitOβπΆ)) β (π΅ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) |
9 | 7, 8 | mpdan 686 |
. . . 4
β’ (π β (π΅ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) |
10 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π΅ β (π΄(Hom βπΆ)π) = (π΄(Hom βπΆ)π΅)) |
11 | 10 | eleq2d 2824 |
. . . . . . . . 9
β’ (π = π΅ β (π β (π΄(Hom βπΆ)π) β π β (π΄(Hom βπΆ)π΅))) |
12 | 11 | eubidv 2585 |
. . . . . . . 8
β’ (π = π΅ β (β!π π β (π΄(Hom βπΆ)π) β β!π π β (π΄(Hom βπΆ)π΅))) |
13 | 12 | rspcv 3580 |
. . . . . . 7
β’ (π΅ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π) β β!π π β (π΄(Hom βπΆ)π΅))) |
14 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(IsoβπΆ) =
(IsoβπΆ) |
15 | 4 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β πΆ β Cat) |
16 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β π΄ β (BaseβπΆ)) |
17 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β π΅ β (BaseβπΆ)) |
18 | 2, 3, 14, 15, 16, 17 | isohom 17666 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (π΄(IsoβπΆ)π΅) β (π΄(Hom βπΆ)π΅)) |
19 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ (β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) β (π΄(IsoβπΆ)π΅) β (π΄(Hom βπΆ)π΅)) |
20 | | euex 2576 |
. . . . . . . . . . . . . . 15
β’
(β!π π β (π΄(Hom βπΆ)π΅) β βπ π β (π΄(Hom βπΆ)π΅)) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (β!π π β (π΄(Hom βπΆ)π΅) β βπ π β (π΄(Hom βπΆ)π΅))) |
22 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π΄ β (π΅(Hom βπΆ)π) = (π΅(Hom βπΆ)π΄)) |
23 | 22 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π΄ β (π β (π΅(Hom βπΆ)π) β π β (π΅(Hom βπΆ)π΄))) |
24 | 23 | eubidv 2585 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π΄ β (β!π π β (π΅(Hom βπΆ)π) β β!π π β (π΅(Hom βπΆ)π΄))) |
25 | 24 | rspcva 3582 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β β!π π β (π΅(Hom βπΆ)π΄)) |
26 | | euex 2576 |
. . . . . . . . . . . . . . . . 17
β’
(β!π π β (π΅(Hom βπΆ)π΄) β βπ π β (π΅(Hom βπΆ)π΄)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β βπ π β (π΅(Hom βπΆ)π΄)) |
28 | 27 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π) β βπ π β (π΅(Hom βπΆ)π΄))) |
29 | 28 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π) β βπ π β (π΅(Hom βπΆ)π΄))) |
30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(InvβπΆ) =
(InvβπΆ) |
31 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β§ π β (π΄(Hom βπΆ)π΅)) β πΆ β Cat) |
32 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β§ π β (π΄(Hom βπΆ)π΅)) β π΄ β (BaseβπΆ)) |
33 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β§ π β (π΄(Hom βπΆ)π΅)) β π΅ β (BaseβπΆ)) |
34 | 4, 1, 7 | 2initoinv 17903 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (π΅(Hom βπΆ)π΄) β§ π β (π΄(Hom βπΆ)π΅)) β π(π΄(InvβπΆ)π΅)π) |
35 | 34 | ad4ant134 1175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β§ π β (π΄(Hom βπΆ)π΅)) β π(π΄(InvβπΆ)π΅)π) |
36 | 2, 30, 31, 32, 33, 14, 35 | inviso1 17656 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β§ π β (π΄(Hom βπΆ)π΅)) β π β (π΄(IsoβπΆ)π΅)) |
37 | 36 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β (π β (π΄(Hom βπΆ)π΅) β π β (π΄(IsoβπΆ)π΅))) |
38 | 37 | eximdv 1921 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ π β (π΅(Hom βπΆ)π΄)) β (βπ π β (π΄(Hom βπΆ)π΅) β βπ π β (π΄(IsoβπΆ)π΅))) |
39 | 38 | expcom 415 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅(Hom βπΆ)π΄) β ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (βπ π β (π΄(Hom βπΆ)π΅) β βπ π β (π΄(IsoβπΆ)π΅)))) |
40 | 39 | exlimiv 1934 |
. . . . . . . . . . . . . . . 16
β’
(βπ π β (π΅(Hom βπΆ)π΄) β ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (βπ π β (π΄(Hom βπΆ)π΅) β βπ π β (π΄(IsoβπΆ)π΅)))) |
41 | 40 | com3l 89 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β (βπ π β (π΄(Hom βπΆ)π΅) β (βπ π β (π΅(Hom βπΆ)π΄) β βπ π β (π΄(IsoβπΆ)π΅)))) |
42 | 41 | impd 412 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β ((βπ π β (π΄(Hom βπΆ)π΅) β§ βπ π β (π΅(Hom βπΆ)π΄)) β βπ π β (π΄(IsoβπΆ)π΅))) |
43 | 21, 29, 42 | syl2and 609 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β ((β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β βπ π β (π΄(IsoβπΆ)π΅))) |
44 | 43 | imp 408 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ (β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) β βπ π β (π΄(IsoβπΆ)π΅)) |
45 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ (β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) β β!π π β (π΄(Hom βπΆ)π΅)) |
46 | | euelss 4286 |
. . . . . . . . . . . 12
β’ (((π΄(IsoβπΆ)π΅) β (π΄(Hom βπΆ)π΅) β§ βπ π β (π΄(IsoβπΆ)π΅) β§ β!π π β (π΄(Hom βπΆ)π΅)) β β!π π β (π΄(IsoβπΆ)π΅)) |
47 | 19, 44, 45, 46 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β (BaseβπΆ) β§ π΄ β (BaseβπΆ))) β§ (β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π))) β β!π π β (π΄(IsoβπΆ)π΅)) |
48 | 47 | exp42 437 |
. . . . . . . . . 10
β’ (π β (π΅ β (BaseβπΆ) β (π΄ β (BaseβπΆ) β ((β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β β!π π β (π΄(IsoβπΆ)π΅))))) |
49 | 48 | com24 95 |
. . . . . . . . 9
β’ (π β ((β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β (π΄ β (BaseβπΆ) β (π΅ β (BaseβπΆ) β β!π π β (π΄(IsoβπΆ)π΅))))) |
50 | 49 | com14 96 |
. . . . . . . 8
β’ (π΅ β (BaseβπΆ) β ((β!π π β (π΄(Hom βπΆ)π΅) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β (π΄ β (BaseβπΆ) β (π β β!π π β (π΄(IsoβπΆ)π΅))))) |
51 | 50 | expd 417 |
. . . . . . 7
β’ (π΅ β (BaseβπΆ) β (β!π π β (π΄(Hom βπΆ)π΅) β (βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π) β (π΄ β (BaseβπΆ) β (π β β!π π β (π΄(IsoβπΆ)π΅)))))) |
52 | 13, 51 | syldc 48 |
. . . . . 6
β’
(βπ β
(BaseβπΆ)β!π π β (π΄(Hom βπΆ)π) β (π΅ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π) β (π΄ β (BaseβπΆ) β (π β β!π π β (π΄(IsoβπΆ)π΅)))))) |
53 | 52 | com15 101 |
. . . . 5
β’ (π β (π΅ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π) β (π΄ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π) β β!π π β (π΄(IsoβπΆ)π΅)))))) |
54 | 53 | impd 412 |
. . . 4
β’ (π β ((π΅ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΅(Hom βπΆ)π)) β (π΄ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π) β β!π π β (π΄(IsoβπΆ)π΅))))) |
55 | 9, 54 | mpd 15 |
. . 3
β’ (π β (π΄ β (BaseβπΆ) β (βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π) β β!π π β (π΄(IsoβπΆ)π΅)))) |
56 | 55 | impd 412 |
. 2
β’ (π β ((π΄ β (BaseβπΆ) β§ βπ β (BaseβπΆ)β!π π β (π΄(Hom βπΆ)π)) β β!π π β (π΄(IsoβπΆ)π΅))) |
57 | 6, 56 | mpd 15 |
1
β’ (π β β!π π β (π΄(IsoβπΆ)π΅)) |