Step | Hyp | Ref
| Expression |
1 | | isinitoi.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | isinitoi.h |
. . 3
β’ π» = (Hom βπΆ) |
3 | | isinitoi.c |
. . 3
β’ (π β πΆ β Cat) |
4 | 1, 2, 3 | isinitoi 17959 |
. 2
β’ ((π β§ π β (InitOβπΆ)) β (π β π΅ β§ βπ β π΅ β!β β β (ππ»π))) |
5 | | oveq2 7412 |
. . . . . . . 8
β’ (π = π β (ππ»π) = (ππ»π)) |
6 | 5 | eleq2d 2813 |
. . . . . . 7
β’ (π = π β (β β (ππ»π) β β β (ππ»π))) |
7 | 6 | eubidv 2574 |
. . . . . 6
β’ (π = π β (β!β β β (ππ»π) β β!β β β (ππ»π))) |
8 | 7 | rspcv 3602 |
. . . . 5
β’ (π β π΅ β (βπ β π΅ β!β β β (ππ»π) β β!β β β (ππ»π))) |
9 | 8 | adantl 481 |
. . . 4
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (βπ β π΅ β!β β β (ππ»π) β β!β β β (ππ»π))) |
10 | | eusn 4729 |
. . . . 5
β’
(β!β β β (ππ»π) β ββ(ππ»π) = {β}) |
11 | | eqid 2726 |
. . . . . . . . 9
β’
(IdβπΆ) =
(IdβπΆ) |
12 | 3 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β πΆ β Cat) |
13 | | simpr 484 |
. . . . . . . . 9
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β π β π΅) |
14 | 1, 2, 11, 12, 13 | catidcl 17633 |
. . . . . . . 8
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β ((IdβπΆ)βπ) β (ππ»π)) |
15 | | fvex 6897 |
. . . . . . . . . . . . 13
β’
((IdβπΆ)βπ) β V |
16 | 15 | elsn 4638 |
. . . . . . . . . . . 12
β’
(((IdβπΆ)βπ) β {β} β ((IdβπΆ)βπ) = β) |
17 | | eqcom 2733 |
. . . . . . . . . . . 12
β’
(((IdβπΆ)βπ) = β β β = ((IdβπΆ)βπ)) |
18 | | sneqbg 4839 |
. . . . . . . . . . . . . 14
β’ (β β V β ({β} = {((IdβπΆ)βπ)} β β = ((IdβπΆ)βπ))) |
19 | 18 | bicomd 222 |
. . . . . . . . . . . . 13
β’ (β β V β (β = ((IdβπΆ)βπ) β {β} = {((IdβπΆ)βπ)})) |
20 | 19 | elv 3474 |
. . . . . . . . . . . 12
β’ (β = ((IdβπΆ)βπ) β {β} = {((IdβπΆ)βπ)}) |
21 | 16, 17, 20 | 3bitri 297 |
. . . . . . . . . . 11
β’
(((IdβπΆ)βπ) β {β} β {β} = {((IdβπΆ)βπ)}) |
22 | 21 | biimpi 215 |
. . . . . . . . . 10
β’
(((IdβπΆ)βπ) β {β} β {β} = {((IdβπΆ)βπ)}) |
23 | 22 | a1i 11 |
. . . . . . . . 9
β’ ((ππ»π) = {β} β (((IdβπΆ)βπ) β {β} β {β} = {((IdβπΆ)βπ)})) |
24 | | eleq2 2816 |
. . . . . . . . 9
β’ ((ππ»π) = {β} β (((IdβπΆ)βπ) β (ππ»π) β ((IdβπΆ)βπ) β {β})) |
25 | | eqeq1 2730 |
. . . . . . . . 9
β’ ((ππ»π) = {β} β ((ππ»π) = {((IdβπΆ)βπ)} β {β} = {((IdβπΆ)βπ)})) |
26 | 23, 24, 25 | 3imtr4d 294 |
. . . . . . . 8
β’ ((ππ»π) = {β} β (((IdβπΆ)βπ) β (ππ»π) β (ππ»π) = {((IdβπΆ)βπ)})) |
27 | 14, 26 | syl5 34 |
. . . . . . 7
β’ ((ππ»π) = {β} β (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (ππ»π) = {((IdβπΆ)βπ)})) |
28 | 27 | exlimiv 1925 |
. . . . . 6
β’
(ββ(ππ»π) = {β} β (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (ππ»π) = {((IdβπΆ)βπ)})) |
29 | 28 | com12 32 |
. . . . 5
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (ββ(ππ»π) = {β} β (ππ»π) = {((IdβπΆ)βπ)})) |
30 | 10, 29 | biimtrid 241 |
. . . 4
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (β!β β β (ππ»π) β (ππ»π) = {((IdβπΆ)βπ)})) |
31 | 9, 30 | syld 47 |
. . 3
β’ (((π β§ π β (InitOβπΆ)) β§ π β π΅) β (βπ β π΅ β!β β β (ππ»π) β (ππ»π) = {((IdβπΆ)βπ)})) |
32 | 31 | expimpd 453 |
. 2
β’ ((π β§ π β (InitOβπΆ)) β ((π β π΅ β§ βπ β π΅ β!β β β (ππ»π)) β (ππ»π) = {((IdβπΆ)βπ)})) |
33 | 4, 32 | mpd 15 |
1
β’ ((π β§ π β (InitOβπΆ)) β (ππ»π) = {((IdβπΆ)βπ)}) |