Step | Hyp | Ref
| Expression |
1 | | ovexd 7397 |
. . 3
β’ (π β (π΄[,)π΅) β V) |
2 | | elhoi.1 |
. . 3
β’ (π β π β π) |
3 | | elmapg 8785 |
. . 3
β’ (((π΄[,)π΅) β V β§ π β π) β (π β ((π΄[,)π΅) βm π) β π:πβΆ(π΄[,)π΅))) |
4 | 1, 2, 3 | syl2anc 585 |
. 2
β’ (π β (π β ((π΄[,)π΅) βm π) β π:πβΆ(π΄[,)π΅))) |
5 | | id 22 |
. . . . . 6
β’ (π:πβΆ(π΄[,)π΅) β π:πβΆ(π΄[,)π΅)) |
6 | | icossxr 13356 |
. . . . . . 7
β’ (π΄[,)π΅) β
β* |
7 | 6 | a1i 11 |
. . . . . 6
β’ (π:πβΆ(π΄[,)π΅) β (π΄[,)π΅) β
β*) |
8 | 5, 7 | fssd 6691 |
. . . . 5
β’ (π:πβΆ(π΄[,)π΅) β π:πβΆβ*) |
9 | | ffvelcdm 7037 |
. . . . . 6
β’ ((π:πβΆ(π΄[,)π΅) β§ π₯ β π) β (πβπ₯) β (π΄[,)π΅)) |
10 | 9 | ralrimiva 3144 |
. . . . 5
β’ (π:πβΆ(π΄[,)π΅) β βπ₯ β π (πβπ₯) β (π΄[,)π΅)) |
11 | 8, 10 | jca 513 |
. . . 4
β’ (π:πβΆ(π΄[,)π΅) β (π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅))) |
12 | | ffn 6673 |
. . . . . . 7
β’ (π:πβΆβ* β π Fn π) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)) β π Fn π) |
14 | | simpr 486 |
. . . . . 6
β’ ((π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)) β βπ₯ β π (πβπ₯) β (π΄[,)π΅)) |
15 | 13, 14 | jca 513 |
. . . . 5
β’ ((π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)) β (π Fn π β§ βπ₯ β π (πβπ₯) β (π΄[,)π΅))) |
16 | | ffnfv 7071 |
. . . . 5
β’ (π:πβΆ(π΄[,)π΅) β (π Fn π β§ βπ₯ β π (πβπ₯) β (π΄[,)π΅))) |
17 | 15, 16 | sylibr 233 |
. . . 4
β’ ((π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)) β π:πβΆ(π΄[,)π΅)) |
18 | 11, 17 | impbii 208 |
. . 3
β’ (π:πβΆ(π΄[,)π΅) β (π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅))) |
19 | 18 | a1i 11 |
. 2
β’ (π β (π:πβΆ(π΄[,)π΅) β (π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)))) |
20 | 4, 19 | bitrd 279 |
1
β’ (π β (π β ((π΄[,)π΅) βm π) β (π:πβΆβ* β§
βπ₯ β π (πβπ₯) β (π΄[,)π΅)))) |