Step | Hyp | Ref
| Expression |
1 | | ulmcl 25756 |
. . . 4
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
2 | 1 | adantr 482 |
. . 3
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β πΊ:πβΆβ) |
3 | 2 | ffnd 6674 |
. 2
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β πΊ Fn π) |
4 | | ulmcl 25756 |
. . . 4
β’ (πΉ(βπ’βπ)π» β π»:πβΆβ) |
5 | 4 | adantl 483 |
. . 3
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β π»:πβΆβ) |
6 | 5 | ffnd 6674 |
. 2
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β π» Fn π) |
7 | | eqid 2737 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
8 | | simplr 768 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π β
β€) |
9 | | simpr 486 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β πΉ:(β€β₯βπ)βΆ(β
βm π)) |
10 | | simpllr 775 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π₯ β π) |
11 | | fvex 6860 |
. . . . . . 7
β’
(β€β₯βπ) β V |
12 | 11 | mptex 7178 |
. . . . . 6
β’ (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β V |
13 | 12 | a1i 11 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β V) |
14 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | fveq1d 6849 |
. . . . . . . 8
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
16 | | eqid 2737 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) |
17 | | fvex 6860 |
. . . . . . . 8
β’ ((πΉβπ)βπ₯) β V |
18 | 15, 16, 17 | fvmpt 6953 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))βπ) = ((πΉβπ)βπ₯)) |
19 | 18 | eqcomd 2743 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((πΉβπ)βπ₯) = ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))βπ)) |
20 | 19 | adantl 483 |
. . . . 5
β’
((((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β§ π β
(β€β₯βπ)) β ((πΉβπ)βπ₯) = ((π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))βπ)) |
21 | | simp-4l 782 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β πΉ(βπ’βπ)πΊ) |
22 | 7, 8, 9, 10, 13, 20, 21 | ulmclm 25762 |
. . . 4
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β (πΊβπ₯)) |
23 | | simp-4r 783 |
. . . . 5
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β πΉ(βπ’βπ)π») |
24 | 7, 8, 9, 10, 13, 20, 23 | ulmclm 25762 |
. . . 4
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β (π»βπ₯)) |
25 | | climuni 15441 |
. . . 4
β’ (((π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β (πΊβπ₯) β§ (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β (π»βπ₯)) β (πΊβπ₯) = (π»βπ₯)) |
26 | 22, 24, 25 | syl2anc 585 |
. . 3
β’
(((((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β§ π β β€) β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β (πΊβπ₯) = (π»βπ₯)) |
27 | | ulmf 25757 |
. . . 4
β’ (πΉ(βπ’βπ)πΊ β βπ β β€ πΉ:(β€β₯βπ)βΆ(β
βm π)) |
28 | 27 | ad2antrr 725 |
. . 3
β’ (((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β βπ β β€ πΉ:(β€β₯βπ)βΆ(β
βm π)) |
29 | 26, 28 | r19.29a 3160 |
. 2
β’ (((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β§ π₯ β π) β (πΊβπ₯) = (π»βπ₯)) |
30 | 3, 6, 29 | eqfnfvd 6990 |
1
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β πΊ = π») |