Step | Hyp | Ref
| Expression |
1 | | refeq.f |
. . 3
β’ (π β πΉ:ββΆβ) |
2 | 1 | ffnd 5366 |
. 2
β’ (π β πΉ Fn β) |
3 | | refeq.g |
. . 3
β’ (π β πΊ:ββΆβ) |
4 | 3 | ffnd 5366 |
. 2
β’ (π β πΊ Fn β) |
5 | | refeq.0 |
. . . . . 6
β’ (π β (πΉβ0) = (πΊβ0)) |
6 | 5 | ad2antrr 488 |
. . . . 5
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβ0) = (πΊβ0)) |
7 | | simplr 528 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β π₯ β β) |
8 | | 0red 7957 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β 0 β β) |
9 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβπ₯) # (πΊβπ₯)) |
10 | 1 | ffvelcdmda 5651 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
11 | 10 | recnd 7985 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
12 | 11 | adantr 276 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβπ₯) β β) |
13 | 3 | ffvelcdmda 5651 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (πΊβπ₯) β β) |
14 | 13 | recnd 7985 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (πΊβπ₯) β β) |
15 | 14 | adantr 276 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΊβπ₯) β β) |
16 | | apne 8579 |
. . . . . . . . . . . 12
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β) β ((πΉβπ₯) # (πΊβπ₯) β (πΉβπ₯) β (πΊβπ₯))) |
17 | 12, 15, 16 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β ((πΉβπ₯) # (πΊβπ₯) β (πΉβπ₯) β (πΊβπ₯))) |
18 | 9, 17 | mpd 13 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβπ₯) β (πΊβπ₯)) |
19 | 18 | neneqd 2368 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β Β¬ (πΉβπ₯) = (πΊβπ₯)) |
20 | | refeq.gt0 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β (0 < π₯ β (πΉβπ₯) = (πΊβπ₯))) |
21 | 20 | r19.21bi 2565 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (0 < π₯ β (πΉβπ₯) = (πΊβπ₯))) |
22 | 21 | adantr 276 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (0 < π₯ β (πΉβπ₯) = (πΊβπ₯))) |
23 | 19, 22 | mtod 663 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β Β¬ 0 < π₯) |
24 | 7, 8, 23 | nltled 8077 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β π₯ β€ 0) |
25 | | refeq.lt0 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β (π₯ < 0 β (πΉβπ₯) = (πΊβπ₯))) |
26 | 25 | r19.21bi 2565 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (π₯ < 0 β (πΉβπ₯) = (πΊβπ₯))) |
27 | 26 | adantr 276 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (π₯ < 0 β (πΉβπ₯) = (πΊβπ₯))) |
28 | 19, 27 | mtod 663 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β Β¬ π₯ < 0) |
29 | 8, 7, 28 | nltled 8077 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β 0 β€ π₯) |
30 | 7, 8 | letri3d 8072 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (π₯ = 0 β (π₯ β€ 0 β§ 0 β€ π₯))) |
31 | 24, 29, 30 | mpbir2and 944 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β π₯ = 0) |
32 | 31 | fveq2d 5519 |
. . . . 5
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβπ₯) = (πΉβ0)) |
33 | 31 | fveq2d 5519 |
. . . . 5
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΊβπ₯) = (πΊβ0)) |
34 | 6, 32, 33 | 3eqtr4d 2220 |
. . . 4
β’ (((π β§ π₯ β β) β§ (πΉβπ₯) # (πΊβπ₯)) β (πΉβπ₯) = (πΊβπ₯)) |
35 | 34, 19 | pm2.65da 661 |
. . 3
β’ ((π β§ π₯ β β) β Β¬ (πΉβπ₯) # (πΊβπ₯)) |
36 | | apti 8578 |
. . . 4
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β) β ((πΉβπ₯) = (πΊβπ₯) β Β¬ (πΉβπ₯) # (πΊβπ₯))) |
37 | 11, 14, 36 | syl2anc 411 |
. . 3
β’ ((π β§ π₯ β β) β ((πΉβπ₯) = (πΊβπ₯) β Β¬ (πΉβπ₯) # (πΊβπ₯))) |
38 | 35, 37 | mpbird 167 |
. 2
β’ ((π β§ π₯ β β) β (πΉβπ₯) = (πΊβπ₯)) |
39 | 2, 4, 38 | eqfnfvd 5616 |
1
β’ (π β πΉ = πΊ) |