Step | Hyp | Ref
| Expression |
1 | | coapm.o |
. . . . . 6
β’ Β· =
(compaβπΆ) |
2 | | coapm.a |
. . . . . 6
β’ π΄ = (ArrowβπΆ) |
3 | | eqid 2733 |
. . . . . 6
β’
(compβπΆ) =
(compβπΆ) |
4 | 1, 2, 3 | coafval 17958 |
. . . . 5
β’ Β· =
(π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπΆ)(codaβπ))(2nd βπ))β©) |
5 | 4 | mpofun 7484 |
. . . 4
β’ Fun Β· |
6 | | funfn 6535 |
. . . 4
β’ (Fun
Β·
β Β· Fn dom Β·
) |
7 | 5, 6 | mpbi 229 |
. . 3
β’ Β· Fn dom
Β· |
8 | 1, 2 | dmcoass 17960 |
. . . . . . . . 9
β’ dom Β·
β (π΄ Γ π΄) |
9 | 8 | sseli 3944 |
. . . . . . . 8
β’ (π§ β dom Β· β π§ β (π΄ Γ π΄)) |
10 | | 1st2nd2 7964 |
. . . . . . . 8
β’ (π§ β (π΄ Γ π΄) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ (π§ β dom Β· β π§ = β¨(1st
βπ§), (2nd
βπ§)β©) |
12 | 11 | fveq2d 6850 |
. . . . . 6
β’ (π§ β dom Β· β ( Β·
βπ§) = ( Β·
ββ¨(1st βπ§), (2nd βπ§)β©)) |
13 | | df-ov 7364 |
. . . . . 6
β’
((1st βπ§) Β· (2nd
βπ§)) = ( Β·
ββ¨(1st βπ§), (2nd βπ§)β©) |
14 | 12, 13 | eqtr4di 2791 |
. . . . 5
β’ (π§ β dom Β· β ( Β·
βπ§) =
((1st βπ§)
Β·
(2nd βπ§))) |
15 | | eqid 2733 |
. . . . . . 7
β’
(HomaβπΆ) = (HomaβπΆ) |
16 | 2, 15 | homarw 17940 |
. . . . . 6
β’
((domaβ(2nd βπ§))(HomaβπΆ)(codaβ(1st
βπ§))) β π΄ |
17 | | id 22 |
. . . . . . . . . . . . 13
β’ (π§ β dom Β· β π§ β dom Β· ) |
18 | 11, 17 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’ (π§ β dom Β· β
β¨(1st βπ§), (2nd βπ§)β© β dom Β· ) |
19 | | df-br 5110 |
. . . . . . . . . . . 12
β’
((1st βπ§)dom Β· (2nd
βπ§) β
β¨(1st βπ§), (2nd βπ§)β© β dom Β· ) |
20 | 18, 19 | sylibr 233 |
. . . . . . . . . . 11
β’ (π§ β dom Β· β
(1st βπ§)dom Β· (2nd
βπ§)) |
21 | 1, 2 | eldmcoa 17959 |
. . . . . . . . . . 11
β’
((1st βπ§)dom Β· (2nd
βπ§) β
((2nd βπ§)
β π΄ β§
(1st βπ§)
β π΄ β§
(codaβ(2nd βπ§)) =
(domaβ(1st βπ§)))) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . 10
β’ (π§ β dom Β· β
((2nd βπ§)
β π΄ β§
(1st βπ§)
β π΄ β§
(codaβ(2nd βπ§)) =
(domaβ(1st βπ§)))) |
23 | 22 | simp1d 1143 |
. . . . . . . . 9
β’ (π§ β dom Β· β
(2nd βπ§)
β π΄) |
24 | 2, 15 | arwhoma 17939 |
. . . . . . . . 9
β’
((2nd βπ§) β π΄ β (2nd βπ§) β
((domaβ(2nd βπ§))(HomaβπΆ)(codaβ(2nd
βπ§)))) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
β’ (π§ β dom Β· β
(2nd βπ§)
β ((domaβ(2nd βπ§))(HomaβπΆ)(codaβ(2nd
βπ§)))) |
26 | 22 | simp3d 1145 |
. . . . . . . . 9
β’ (π§ β dom Β· β
(codaβ(2nd βπ§)) =
(domaβ(1st βπ§))) |
27 | 26 | oveq2d 7377 |
. . . . . . . 8
β’ (π§ β dom Β· β
((domaβ(2nd βπ§))(HomaβπΆ)(codaβ(2nd
βπ§))) =
((domaβ(2nd βπ§))(HomaβπΆ)(domaβ(1st
βπ§)))) |
28 | 25, 27 | eleqtrd 2836 |
. . . . . . 7
β’ (π§ β dom Β· β
(2nd βπ§)
β ((domaβ(2nd βπ§))(HomaβπΆ)(domaβ(1st
βπ§)))) |
29 | 22 | simp2d 1144 |
. . . . . . . 8
β’ (π§ β dom Β· β
(1st βπ§)
β π΄) |
30 | 2, 15 | arwhoma 17939 |
. . . . . . . 8
β’
((1st βπ§) β π΄ β (1st βπ§) β
((domaβ(1st βπ§))(HomaβπΆ)(codaβ(1st
βπ§)))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
β’ (π§ β dom Β· β
(1st βπ§)
β ((domaβ(1st βπ§))(HomaβπΆ)(codaβ(1st
βπ§)))) |
32 | 1, 15, 28, 31 | coahom 17964 |
. . . . . 6
β’ (π§ β dom Β· β
((1st βπ§)
Β·
(2nd βπ§))
β ((domaβ(2nd βπ§))(HomaβπΆ)(codaβ(1st
βπ§)))) |
33 | 16, 32 | sselid 3946 |
. . . . 5
β’ (π§ β dom Β· β
((1st βπ§)
Β·
(2nd βπ§))
β π΄) |
34 | 14, 33 | eqeltrd 2834 |
. . . 4
β’ (π§ β dom Β· β ( Β·
βπ§) β π΄) |
35 | 34 | rgen 3063 |
. . 3
β’
βπ§ β dom
Β·
( Β· βπ§) β π΄ |
36 | | ffnfv 7070 |
. . 3
β’ ( Β· :dom
Β·
βΆπ΄ β ( Β· Fn dom
Β·
β§ βπ§ β dom
Β·
( Β· βπ§) β π΄)) |
37 | 7, 35, 36 | mpbir2an 710 |
. 2
β’ Β· :dom
Β·
βΆπ΄ |
38 | 2 | fvexi 6860 |
. . 3
β’ π΄ β V |
39 | 38, 38 | xpex 7691 |
. . 3
β’ (π΄ Γ π΄) β V |
40 | 38, 39 | elpm2 8818 |
. 2
β’ ( Β· β
(π΄ βpm
(π΄ Γ π΄)) β ( Β· :dom Β·
βΆπ΄ β§ dom Β·
β (π΄ Γ π΄))) |
41 | 37, 8, 40 | mpbir2an 710 |
1
β’ Β· β
(π΄ βpm
(π΄ Γ π΄)) |