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 | | inrresf 9857 |
. . . 4
β’ (inr
βΎ π΅):π΅βΆ(π΄ β π΅) |
7 | | ffn 6669 |
. . . 4
β’ ((inr
βΎ π΅):π΅βΆ(π΄ β π΅) β (inr βΎ π΅) Fn π΅) |
8 | 6, 7 | mp1i 13 |
. . 3
β’ (π β (inr βΎ π΅) Fn π΅) |
9 | | frn 6676 |
. . . 4
β’ ((inr
βΎ π΅):π΅βΆ(π΄ β π΅) β ran (inr βΎ π΅) β (π΄ β π΅)) |
10 | 6, 9 | mp1i 13 |
. . 3
β’ (π β ran (inr βΎ π΅) β (π΄ β π΅)) |
11 | | fnco 6619 |
. . 3
β’ ((π» Fn (π΄ β π΅) β§ (inr βΎ π΅) Fn π΅ β§ ran (inr βΎ π΅) β (π΄ β π΅)) β (π» β (inr βΎ π΅)) Fn π΅) |
12 | 5, 8, 10, 11 | syl3anc 1372 |
. 2
β’ (π β (π» β (inr βΎ π΅)) Fn π΅) |
13 | 2 | ffnd 6670 |
. 2
β’ (π β πΊ Fn π΅) |
14 | | fvco2 6939 |
. . . 4
β’ (((inr
βΎ π΅) Fn π΅ β§ π β π΅) β ((π» β (inr βΎ π΅))βπ) = (π»β((inr βΎ π΅)βπ))) |
15 | 8, 14 | sylan 581 |
. . 3
β’ ((π β§ π β π΅) β ((π» β (inr βΎ π΅))βπ) = (π»β((inr βΎ π΅)βπ))) |
16 | | fvres 6862 |
. . . . . 6
β’ (π β π΅ β ((inr βΎ π΅)βπ) = (inrβπ)) |
17 | 16 | adantl 483 |
. . . . 5
β’ ((π β§ π β π΅) β ((inr βΎ π΅)βπ) = (inrβπ)) |
18 | 17 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β π΅) β (π»β((inr βΎ π΅)βπ)) = (π»β(inrβπ))) |
19 | | fveqeq2 6852 |
. . . . . . . 8
β’ (π₯ = (inrβπ) β ((1st βπ₯) = β
β
(1st β(inrβπ)) = β
)) |
20 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = (inrβπ) β (πΉβ(2nd βπ₯)) = (πΉβ(2nd
β(inrβπ)))) |
21 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π₯ = (inrβπ) β (πΊβ(2nd βπ₯)) = (πΊβ(2nd
β(inrβπ)))) |
22 | 19, 20, 21 | ifbieq12d 4515 |
. . . . . . 7
β’ (π₯ = (inrβπ) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = if((1st
β(inrβπ)) =
β
, (πΉβ(2nd
β(inrβπ))),
(πΊβ(2nd
β(inrβπ))))) |
23 | 22 | adantl 483 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π₯ = (inrβπ)) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = if((1st
β(inrβπ)) =
β
, (πΉβ(2nd
β(inrβπ))),
(πΊβ(2nd
β(inrβπ))))) |
24 | | 1stinr 9870 |
. . . . . . . . . 10
β’ (π β π΅ β (1st
β(inrβπ)) =
1o) |
25 | | 1n0 8435 |
. . . . . . . . . . . 12
β’
1o β β
|
26 | 25 | neii 2942 |
. . . . . . . . . . 11
β’ Β¬
1o = β
|
27 | | eqeq1 2737 |
. . . . . . . . . . 11
β’
((1st β(inrβπ)) = 1o β ((1st
β(inrβπ)) =
β
β 1o = β
)) |
28 | 26, 27 | mtbiri 327 |
. . . . . . . . . 10
β’
((1st β(inrβπ)) = 1o β Β¬
(1st β(inrβπ)) = β
) |
29 | 24, 28 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β Β¬ (1st
β(inrβπ)) =
β
) |
30 | 29 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β π΅) β Β¬ (1st
β(inrβπ)) =
β
) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ = (inrβπ)) β Β¬ (1st
β(inrβπ)) =
β
) |
32 | 31 | iffalsed 4498 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π₯ = (inrβπ)) β if((1st
β(inrβπ)) =
β
, (πΉβ(2nd
β(inrβπ))),
(πΊβ(2nd
β(inrβπ)))) =
(πΊβ(2nd
β(inrβπ)))) |
33 | 23, 32 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π β π΅) β§ π₯ = (inrβπ)) β if((1st βπ₯) = β
, (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯))) = (πΊβ(2nd
β(inrβπ)))) |
34 | | djurcl 9852 |
. . . . . 6
β’ (π β π΅ β (inrβπ) β (π΄ β π΅)) |
35 | 34 | adantl 483 |
. . . . 5
β’ ((π β§ π β π΅) β (inrβπ) β (π΄ β π΅)) |
36 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β πΊ:π΅βΆπΆ) |
37 | | 2ndinr 9871 |
. . . . . . . 8
β’ (π β π΅ β (2nd
β(inrβπ)) =
π) |
38 | 37 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β π΅) β (2nd
β(inrβπ)) =
π) |
39 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β π΅) β π β π΅) |
40 | 38, 39 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β π΅) β (2nd
β(inrβπ))
β π΅) |
41 | 36, 40 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ π β π΅) β (πΊβ(2nd
β(inrβπ)))
β πΆ) |
42 | 3, 33, 35, 41 | fvmptd2 6957 |
. . . 4
β’ ((π β§ π β π΅) β (π»β(inrβπ)) = (πΊβ(2nd
β(inrβπ)))) |
43 | 18, 42 | eqtrd 2773 |
. . 3
β’ ((π β§ π β π΅) β (π»β((inr βΎ π΅)βπ)) = (πΊβ(2nd
β(inrβπ)))) |
44 | 38 | fveq2d 6847 |
. . 3
β’ ((π β§ π β π΅) β (πΊβ(2nd
β(inrβπ))) =
(πΊβπ)) |
45 | 15, 43, 44 | 3eqtrd 2777 |
. 2
β’ ((π β§ π β π΅) β ((π» β (inr βΎ π΅))βπ) = (πΊβπ)) |
46 | 12, 13, 45 | eqfnfvd 6986 |
1
β’ (π β (π» β (inr βΎ π΅)) = πΊ) |