Step | Hyp | Ref
| Expression |
1 | | lo1dm 15410 |
. . 3
β’ ((π₯ β π΄ β¦ π΅) β β€π(1) β dom (π₯ β π΄ β¦ π΅) β β) |
2 | | eqid 2733 |
. . . . 5
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
3 | | lo1eq.1 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β β) |
4 | 2, 3 | dmmptd 6650 |
. . . 4
β’ (π β dom (π₯ β π΄ β¦ π΅) = π΄) |
5 | 4 | sseq1d 3979 |
. . 3
β’ (π β (dom (π₯ β π΄ β¦ π΅) β β β π΄ β β)) |
6 | 1, 5 | imbitrid 243 |
. 2
β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β π΄ β
β)) |
7 | | lo1dm 15410 |
. . 3
β’ ((π₯ β π΄ β¦ πΆ) β β€π(1) β dom (π₯ β π΄ β¦ πΆ) β β) |
8 | | eqid 2733 |
. . . . 5
β’ (π₯ β π΄ β¦ πΆ) = (π₯ β π΄ β¦ πΆ) |
9 | | lo1eq.2 |
. . . . 5
β’ ((π β§ π₯ β π΄) β πΆ β β) |
10 | 8, 9 | dmmptd 6650 |
. . . 4
β’ (π β dom (π₯ β π΄ β¦ πΆ) = π΄) |
11 | 10 | sseq1d 3979 |
. . 3
β’ (π β (dom (π₯ β π΄ β¦ πΆ) β β β π΄ β β)) |
12 | 7, 11 | imbitrid 243 |
. 2
β’ (π β ((π₯ β π΄ β¦ πΆ) β β€π(1) β π΄ β
β)) |
13 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β π₯ β (π΄ β© (π·[,)+β))) |
14 | | elin 3930 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄ β© (π·[,)+β)) β (π₯ β π΄ β§ π₯ β (π·[,)+β))) |
15 | 13, 14 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β (π₯ β π΄ β§ π₯ β (π·[,)+β))) |
16 | 15 | simpld 496 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β π₯ β π΄) |
17 | 15 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β π₯ β (π·[,)+β)) |
18 | | lo1eq.3 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β β) |
19 | | elicopnf 13371 |
. . . . . . . . . . . . . . . 16
β’ (π· β β β (π₯ β (π·[,)+β) β (π₯ β β β§ π· β€ π₯))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π₯ β (π·[,)+β) β (π₯ β β β§ π· β€ π₯))) |
21 | 20 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π·[,)+β)) β (π₯ β β β§ π· β€ π₯)) |
22 | 17, 21 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β (π₯ β β β§ π· β€ π₯)) |
23 | 22 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β π· β€ π₯) |
24 | 16, 23 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β (π₯ β π΄ β§ π· β€ π₯)) |
25 | | lo1eq.4 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΄ β§ π· β€ π₯)) β π΅ = πΆ) |
26 | 24, 25 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β© (π·[,)+β))) β π΅ = πΆ) |
27 | 26 | mpteq2dva 5209 |
. . . . . . . . 9
β’ (π β (π₯ β (π΄ β© (π·[,)+β)) β¦ π΅) = (π₯ β (π΄ β© (π·[,)+β)) β¦ πΆ)) |
28 | | inss1 4192 |
. . . . . . . . . 10
β’ (π΄ β© (π·[,)+β)) β π΄ |
29 | | resmpt 5995 |
. . . . . . . . . 10
β’ ((π΄ β© (π·[,)+β)) β π΄ β ((π₯ β π΄ β¦ π΅) βΎ (π΄ β© (π·[,)+β))) = (π₯ β (π΄ β© (π·[,)+β)) β¦ π΅)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ π΅) βΎ (π΄ β© (π·[,)+β))) = (π₯ β (π΄ β© (π·[,)+β)) β¦ π΅) |
31 | | resmpt 5995 |
. . . . . . . . . 10
β’ ((π΄ β© (π·[,)+β)) β π΄ β ((π₯ β π΄ β¦ πΆ) βΎ (π΄ β© (π·[,)+β))) = (π₯ β (π΄ β© (π·[,)+β)) β¦ πΆ)) |
32 | 28, 31 | ax-mp 5 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ πΆ) βΎ (π΄ β© (π·[,)+β))) = (π₯ β (π΄ β© (π·[,)+β)) β¦ πΆ) |
33 | 27, 30, 32 | 3eqtr4g 2798 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ π΅) βΎ (π΄ β© (π·[,)+β))) = ((π₯ β π΄ β¦ πΆ) βΎ (π΄ β© (π·[,)+β)))) |
34 | | resres 5954 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ π΅) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ π΅) βΎ (π΄ β© (π·[,)+β))) |
35 | | resres 5954 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ πΆ) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ πΆ) βΎ (π΄ β© (π·[,)+β))) |
36 | 33, 34, 35 | 3eqtr4g 2798 |
. . . . . . 7
β’ (π β (((π₯ β π΄ β¦ π΅) βΎ π΄) βΎ (π·[,)+β)) = (((π₯ β π΄ β¦ πΆ) βΎ π΄) βΎ (π·[,)+β))) |
37 | | ssid 3970 |
. . . . . . . 8
β’ π΄ β π΄ |
38 | | resmpt 5995 |
. . . . . . . 8
β’ (π΄ β π΄ β ((π₯ β π΄ β¦ π΅) βΎ π΄) = (π₯ β π΄ β¦ π΅)) |
39 | | reseq1 5935 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ π΅) βΎ π΄) = (π₯ β π΄ β¦ π΅) β (((π₯ β π΄ β¦ π΅) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β))) |
40 | 37, 38, 39 | mp2b 10 |
. . . . . . 7
β’ (((π₯ β π΄ β¦ π΅) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β)) |
41 | | resmpt 5995 |
. . . . . . . 8
β’ (π΄ β π΄ β ((π₯ β π΄ β¦ πΆ) βΎ π΄) = (π₯ β π΄ β¦ πΆ)) |
42 | | reseq1 5935 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ πΆ) βΎ π΄) = (π₯ β π΄ β¦ πΆ) β (((π₯ β π΄ β¦ πΆ) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β))) |
43 | 37, 41, 42 | mp2b 10 |
. . . . . . 7
β’ (((π₯ β π΄ β¦ πΆ) βΎ π΄) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β)) |
44 | 36, 40, 43 | 3eqtr3g 2796 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β)) = ((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β))) |
45 | 44 | eleq1d 2819 |
. . . . 5
β’ (π β (((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β)) β β€π(1) β
((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β)) β
β€π(1))) |
46 | 45 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β β) β (((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β)) β β€π(1) β
((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β)) β
β€π(1))) |
47 | 3 | fmpttd 7067 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
48 | 47 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
49 | | simpr 486 |
. . . . 5
β’ ((π β§ π΄ β β) β π΄ β β) |
50 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β π· β β) |
51 | 48, 49, 50 | lo1resb 15455 |
. . . 4
β’ ((π β§ π΄ β β) β ((π₯ β π΄ β¦ π΅) β β€π(1) β ((π₯ β π΄ β¦ π΅) βΎ (π·[,)+β)) β
β€π(1))) |
52 | 9 | fmpttd 7067 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ πΆ):π΄βΆβ) |
53 | 52 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β (π₯ β π΄ β¦ πΆ):π΄βΆβ) |
54 | 53, 49, 50 | lo1resb 15455 |
. . . 4
β’ ((π β§ π΄ β β) β ((π₯ β π΄ β¦ πΆ) β β€π(1) β ((π₯ β π΄ β¦ πΆ) βΎ (π·[,)+β)) β
β€π(1))) |
55 | 46, 51, 54 | 3bitr4d 311 |
. . 3
β’ ((π β§ π΄ β β) β ((π₯ β π΄ β¦ π΅) β β€π(1) β (π₯ β π΄ β¦ πΆ) β β€π(1))) |
56 | 55 | ex 414 |
. 2
β’ (π β (π΄ β β β ((π₯ β π΄ β¦ π΅) β β€π(1) β (π₯ β π΄ β¦ πΆ) β
β€π(1)))) |
57 | 6, 12, 56 | pm5.21ndd 381 |
1
β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β (π₯ β π΄ β¦ πΆ) β β€π(1))) |