Step | Hyp | Ref
| Expression |
1 | | updjud.f |
. . . . 5
β’ (π β πΉ:π΄βΆπΆ) |
2 | | updjud.g |
. . . . 5
β’ (π β πΊ:π΅βΆπΆ) |
3 | | updjudhf.h |
. . . . 5
β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) |
4 | 1, 2, 3 | updjudhf 9872 |
. . . 4
β’ (π β π»:(π΄ β π΅)βΆπΆ) |
5 | 4 | ffnd 6670 |
. . 3
β’ (π β π» Fn (π΄ β π΅)) |
6 | | inlresf 9855 |
. . . 4
β’ (inl
βΎ π΄):π΄βΆ(π΄ β π΅) |
7 | | ffn 6669 |
. . . 4
β’ ((inl
βΎ π΄):π΄βΆ(π΄ β π΅) β (inl βΎ π΄) Fn π΄) |
8 | 6, 7 | mp1i 13 |
. . 3
β’ (π β (inl βΎ π΄) Fn π΄) |
9 | | frn 6676 |
. . . 4
β’ ((inl
βΎ π΄):π΄βΆ(π΄ β π΅) β ran (inl βΎ π΄) β (π΄ β π΅)) |
10 | 6, 9 | mp1i 13 |
. . 3
β’ (π β ran (inl βΎ π΄) β (π΄ β π΅)) |
11 | | fnco 6619 |
. . 3
β’ ((π» Fn (π΄ β π΅) β§ (inl βΎ π΄) Fn π΄ β§ ran (inl βΎ π΄) β (π΄ β π΅)) β (π» β (inl βΎ π΄)) Fn π΄) |
12 | 5, 8, 10, 11 | syl3anc 1372 |
. 2
β’ (π β (π» β (inl βΎ π΄)) Fn π΄) |
13 | 1 | ffnd 6670 |
. 2
β’ (π β πΉ Fn π΄) |
14 | | fvco2 6939 |
. . . 4
β’ (((inl
βΎ π΄) Fn π΄ β§ π β π΄) β ((π» β (inl βΎ π΄))βπ) = (π»β((inl βΎ π΄)βπ))) |
15 | 8, 14 | sylan 581 |
. . 3
β’ ((π β§ π β π΄) β ((π» β (inl βΎ π΄))βπ) = (π»β((inl βΎ π΄)βπ))) |
16 | | fvres 6862 |
. . . . . 6
β’ (π β π΄ β ((inl βΎ π΄)βπ) = (inlβπ)) |
17 | 16 | adantl 483 |
. . . . 5
β’ ((π β§ π β π΄) β ((inl βΎ π΄)βπ) = (inlβπ)) |
18 | 17 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β π΄) β (π»β((inl βΎ π΄)βπ)) = (π»β(inlβπ))) |
19 | | fveqeq2 6852 |
. . . . . . . 8
β’ (π₯ = (inlβπ) β ((1st βπ₯) = β
β
(1st β(inlβπ)) = β
)) |
20 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = (inlβπ) β (πΉβ(2nd βπ₯)) = (πΉβ(2nd
β(inlβπ)))) |
21 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = (inlβπ) β (πΊβ(2nd βπ₯)) = (πΊβ(2nd
β(inlβπ)))) |
22 | 19, 20, 21 | ifbieq12d 4515 |
. . . . . . 7
β’ (π₯ = (inlβπ) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = if((1st
β(inlβπ)) =
β
, (πΉβ(2nd
β(inlβπ))),
(πΊβ(2nd
β(inlβπ))))) |
23 | 22 | adantl 483 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π₯ = (inlβπ)) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = if((1st
β(inlβπ)) =
β
, (πΉβ(2nd
β(inlβπ))),
(πΊβ(2nd
β(inlβπ))))) |
24 | | 1stinl 9868 |
. . . . . . . . 9
β’ (π β π΄ β (1st
β(inlβπ)) =
β
) |
25 | 24 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (1st
β(inlβπ)) =
β
) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π₯ = (inlβπ)) β (1st
β(inlβπ)) =
β
) |
27 | 26 | iftrued 4495 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π₯ = (inlβπ)) β if((1st
β(inlβπ)) =
β
, (πΉβ(2nd
β(inlβπ))),
(πΊβ(2nd
β(inlβπ)))) =
(πΉβ(2nd
β(inlβπ)))) |
28 | 23, 27 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π β π΄) β§ π₯ = (inlβπ)) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = (πΉβ(2nd
β(inlβπ)))) |
29 | | djulcl 9851 |
. . . . . 6
β’ (π β π΄ β (inlβπ) β (π΄ β π΅)) |
30 | 29 | adantl 483 |
. . . . 5
β’ ((π β§ π β π΄) β (inlβπ) β (π΄ β π΅)) |
31 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΉ:π΄βΆπΆ) |
32 | | 2ndinl 9869 |
. . . . . . . 8
β’ (π β π΄ β (2nd
β(inlβπ)) =
π) |
33 | 32 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β π΄) β (2nd
β(inlβπ)) =
π) |
34 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β π΄) |
35 | 33, 34 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β π΄) β (2nd
β(inlβπ))
β π΄) |
36 | 31, 35 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ π β π΄) β (πΉβ(2nd
β(inlβπ)))
β πΆ) |
37 | 3, 28, 30, 36 | fvmptd2 6957 |
. . . 4
β’ ((π β§ π β π΄) β (π»β(inlβπ)) = (πΉβ(2nd
β(inlβπ)))) |
38 | 18, 37 | eqtrd 2773 |
. . 3
β’ ((π β§ π β π΄) β (π»β((inl βΎ π΄)βπ)) = (πΉβ(2nd
β(inlβπ)))) |
39 | 33 | fveq2d 6847 |
. . 3
β’ ((π β§ π β π΄) β (πΉβ(2nd
β(inlβπ))) =
(πΉβπ)) |
40 | 15, 38, 39 | 3eqtrd 2777 |
. 2
β’ ((π β§ π β π΄) β ((π» β (inl βΎ π΄))βπ) = (πΉβπ)) |
41 | 12, 13, 40 | eqfnfvd 6986 |
1
β’ (π β (π» β (inl βΎ π΄)) = πΉ) |