Step | Hyp | Ref
| Expression |
1 | | fss 6686 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π΅ β On) β πΉ:π΄βΆOn) |
2 | 1 | ex 414 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (π΅ β On β πΉ:π΄βΆOn)) |
3 | | fdm 6678 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β dom πΉ = π΄) |
4 | 3 | feq2d 6655 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (πΉ:dom πΉβΆOn β πΉ:π΄βΆOn)) |
5 | 2, 4 | sylibrd 259 |
. . 3
β’ (πΉ:π΄βΆπ΅ β (π΅ β On β πΉ:dom πΉβΆOn)) |
6 | | ordeq 6325 |
. . . . 5
β’ (dom
πΉ = π΄ β (Ord dom πΉ β Ord π΄)) |
7 | 3, 6 | syl 17 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (Ord dom πΉ β Ord π΄)) |
8 | 7 | biimprd 248 |
. . 3
β’ (πΉ:π΄βΆπ΅ β (Ord π΄ β Ord dom πΉ)) |
9 | 3 | raleqdv 3312 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯) β βπ₯ β π΄ βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
10 | 9 | biimprd 248 |
. . 3
β’ (πΉ:π΄βΆπ΅ β (βπ₯ β π΄ βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯) β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
11 | 5, 8, 10 | 3anim123d 1444 |
. 2
β’ (πΉ:π΄βΆπ΅ β ((π΅ β On β§ Ord π΄ β§ βπ₯ β π΄ βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)))) |
12 | | dfsmo2 8294 |
. 2
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
13 | 11, 12 | syl6ibr 252 |
1
β’ (πΉ:π΄βΆπ΅ β ((π΅ β On β§ Ord π΄ β§ βπ₯ β π΄ βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) β Smo πΉ)) |