Step | Hyp | Ref
| Expression |
1 | | catidd.2 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฆ๐ป๐ฅ))) โ ( 1 (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐) |
2 | 1 | ex 414 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฆ๐ป๐ฅ)) โ ( 1 (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐)) |
3 | | catidd.b |
. . . . . . . . . . . 12
โข (๐ โ ๐ต = (Baseโ๐ถ)) |
4 | 3 | eleq2d 2820 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ ๐ต โ ๐ฅ โ (Baseโ๐ถ))) |
5 | 3 | eleq2d 2820 |
. . . . . . . . . . 11
โข (๐ โ (๐ฆ โ ๐ต โ ๐ฆ โ (Baseโ๐ถ))) |
6 | | catidd.h |
. . . . . . . . . . . . 13
โข (๐ โ ๐ป = (Hom โ๐ถ)) |
7 | 6 | oveqd 7426 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฆ๐ป๐ฅ) = (๐ฆ(Hom โ๐ถ)๐ฅ)) |
8 | 7 | eleq2d 2820 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ (๐ฆ๐ป๐ฅ) โ ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ))) |
9 | 4, 5, 8 | 3anbi123d 1437 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฆ๐ป๐ฅ)) โ (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)))) |
10 | | catidd.o |
. . . . . . . . . . . . 13
โข (๐ โ ยท = (compโ๐ถ)) |
11 | 10 | oveqd 7426 |
. . . . . . . . . . . 12
โข (๐ โ (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ) = (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)) |
12 | 11 | oveqd 7426 |
. . . . . . . . . . 11
โข (๐ โ ( 1 (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐)) |
13 | 12 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ โ (( 1 (โจ๐ฆ, ๐ฅโฉ ยท ๐ฅ)๐) = ๐ โ ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐)) |
14 | 2, 9, 13 | 3imtr3d 293 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)) โ ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐)) |
15 | 14 | 3expd 1354 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ (Baseโ๐ถ) โ (๐ฆ โ (Baseโ๐ถ) โ (๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ) โ ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐)))) |
16 | 15 | imp41 427 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ (Baseโ๐ถ)) โง ๐ฆ โ (Baseโ๐ถ)) โง ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)) โ ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐) |
17 | 16 | ralrimiva 3147 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (Baseโ๐ถ)) โง ๐ฆ โ (Baseโ๐ถ)) โ โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐) |
18 | | catidd.3 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฅ๐ป๐ฆ))) โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) 1 ) = ๐) |
19 | 18 | ex 414 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฅ๐ป๐ฆ)) โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) 1 ) = ๐)) |
20 | 6 | oveqd 7426 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ๐ป๐ฆ) = (๐ฅ(Hom โ๐ถ)๐ฆ)) |
21 | 20 | eleq2d 2820 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ (๐ฅ๐ป๐ฆ) โ ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ))) |
22 | 4, 5, 21 | 3anbi123d 1437 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ โ (๐ฅ๐ป๐ฆ)) โ (๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)))) |
23 | 10 | oveqd 7426 |
. . . . . . . . . . . 12
โข (๐ โ (โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) = (โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)) |
24 | 23 | oveqd 7426 |
. . . . . . . . . . 11
โข (๐ โ (๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) 1 ) = (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 )) |
25 | 24 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ โ ((๐(โจ๐ฅ, ๐ฅโฉ ยท ๐ฆ) 1 ) = ๐ โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
26 | 19, 22, 25 | 3imtr3d 293 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ (Baseโ๐ถ) โง ๐ฆ โ (Baseโ๐ถ) โง ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)) โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
27 | 26 | 3expd 1354 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ (Baseโ๐ถ) โ (๐ฆ โ (Baseโ๐ถ) โ (๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ) โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)))) |
28 | 27 | imp41 427 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ (Baseโ๐ถ)) โง ๐ฆ โ (Baseโ๐ถ)) โง ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)) โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐) |
29 | 28 | ralrimiva 3147 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (Baseโ๐ถ)) โง ๐ฆ โ (Baseโ๐ถ)) โ โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐) |
30 | 17, 29 | jca 513 |
. . . . 5
โข (((๐ โง ๐ฅ โ (Baseโ๐ถ)) โง ๐ฆ โ (Baseโ๐ถ)) โ (โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
31 | 30 | ralrimiva 3147 |
. . . 4
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
32 | | catidd.1 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต) โ 1 โ (๐ฅ๐ป๐ฅ)) |
33 | 32 | ex 414 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ต โ 1 โ (๐ฅ๐ป๐ฅ))) |
34 | 6 | oveqd 7426 |
. . . . . . . 8
โข (๐ โ (๐ฅ๐ป๐ฅ) = (๐ฅ(Hom โ๐ถ)๐ฅ)) |
35 | 34 | eleq2d 2820 |
. . . . . . 7
โข (๐ โ ( 1 โ (๐ฅ๐ป๐ฅ) โ 1 โ (๐ฅ(Hom โ๐ถ)๐ฅ))) |
36 | 33, 4, 35 | 3imtr3d 293 |
. . . . . 6
โข (๐ โ (๐ฅ โ (Baseโ๐ถ) โ 1 โ (๐ฅ(Hom โ๐ถ)๐ฅ))) |
37 | 36 | imp 408 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ 1 โ (๐ฅ(Hom โ๐ถ)๐ฅ)) |
38 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
39 | | eqid 2733 |
. . . . . 6
โข (Hom
โ๐ถ) = (Hom
โ๐ถ) |
40 | | eqid 2733 |
. . . . . 6
โข
(compโ๐ถ) =
(compโ๐ถ) |
41 | | catidd.c |
. . . . . . 7
โข (๐ โ ๐ถ โ Cat) |
42 | 41 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ ๐ถ โ Cat) |
43 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ ๐ฅ โ (Baseโ๐ถ)) |
44 | 38, 39, 40, 42, 43 | catideu 17619 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ โ!๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)) |
45 | | oveq1 7416 |
. . . . . . . . . 10
โข (๐ = 1 โ (๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐)) |
46 | 45 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ = 1 โ ((๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โ ( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐)) |
47 | 46 | ralbidv 3178 |
. . . . . . . 8
โข (๐ = 1 โ (โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โ โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐)) |
48 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ = 1 โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 )) |
49 | 48 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ = 1 โ ((๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐ โ (๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
50 | 49 | ralbidv 3178 |
. . . . . . . 8
โข (๐ = 1 โ (โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐ โ โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐)) |
51 | 47, 50 | anbi12d 632 |
. . . . . . 7
โข (๐ = 1 โ ((โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐) โ (โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐))) |
52 | 51 | ralbidv 3178 |
. . . . . 6
โข (๐ = 1 โ (โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐) โ โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐))) |
53 | 52 | riota2 7391 |
. . . . 5
โข (( 1 โ (๐ฅ(Hom โ๐ถ)๐ฅ) โง โ!๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)) โ (โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐) โ (โฉ๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)) = 1 )) |
54 | 37, 44, 53 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ (โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)( 1 (โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ) 1 ) = ๐) โ (โฉ๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)) = 1 )) |
55 | 31, 54 | mpbid 231 |
. . 3
โข ((๐ โง ๐ฅ โ (Baseโ๐ถ)) โ (โฉ๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)) = 1 ) |
56 | 55 | mpteq2dva 5249 |
. 2
โข (๐ โ (๐ฅ โ (Baseโ๐ถ) โฆ (โฉ๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐))) = (๐ฅ โ (Baseโ๐ถ) โฆ 1 )) |
57 | | eqid 2733 |
. . 3
โข
(Idโ๐ถ) =
(Idโ๐ถ) |
58 | 38, 39, 40, 41, 57 | cidfval 17620 |
. 2
โข (๐ โ (Idโ๐ถ) = (๐ฅ โ (Baseโ๐ถ) โฆ (โฉ๐ โ (๐ฅ(Hom โ๐ถ)๐ฅ)โ๐ฆ โ (Baseโ๐ถ)(โ๐ โ (๐ฆ(Hom โ๐ถ)๐ฅ)(๐(โจ๐ฆ, ๐ฅโฉ(compโ๐ถ)๐ฅ)๐) = ๐ โง โ๐ โ (๐ฅ(Hom โ๐ถ)๐ฆ)(๐(โจ๐ฅ, ๐ฅโฉ(compโ๐ถ)๐ฆ)๐) = ๐)))) |
59 | 3 | mpteq1d 5244 |
. 2
โข (๐ โ (๐ฅ โ ๐ต โฆ 1 ) = (๐ฅ โ (Baseโ๐ถ) โฆ 1 )) |
60 | 56, 58, 59 | 3eqtr4d 2783 |
1
โข (๐ โ (Idโ๐ถ) = (๐ฅ โ ๐ต โฆ 1 )) |