Step | Hyp | Ref
| Expression |
1 | | dfsmo2 8294 |
. . . . . . 7
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
2 | 1 | simp1bi 1146 |
. . . . . 6
β’ (Smo
πΉ β πΉ:dom πΉβΆOn) |
3 | 2 | ffund 6673 |
. . . . 5
β’ (Smo
πΉ β Fun πΉ) |
4 | | funres 6544 |
. . . . . 6
β’ (Fun
πΉ β Fun (πΉ βΎ π΄)) |
5 | 4 | funfnd 6533 |
. . . . 5
β’ (Fun
πΉ β (πΉ βΎ π΄) Fn dom (πΉ βΎ π΄)) |
6 | 3, 5 | syl 17 |
. . . 4
β’ (Smo
πΉ β (πΉ βΎ π΄) Fn dom (πΉ βΎ π΄)) |
7 | | df-ima 5647 |
. . . . . 6
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
8 | | imassrn 6025 |
. . . . . 6
β’ (πΉ β π΄) β ran πΉ |
9 | 7, 8 | eqsstrri 3980 |
. . . . 5
β’ ran
(πΉ βΎ π΄) β ran πΉ |
10 | 2 | frnd 6677 |
. . . . 5
β’ (Smo
πΉ β ran πΉ β On) |
11 | 9, 10 | sstrid 3956 |
. . . 4
β’ (Smo
πΉ β ran (πΉ βΎ π΄) β On) |
12 | | df-f 6501 |
. . . 4
β’ ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn β ((πΉ βΎ π΄) Fn dom (πΉ βΎ π΄) β§ ran (πΉ βΎ π΄) β On)) |
13 | 6, 11, 12 | sylanbrc 584 |
. . 3
β’ (Smo
πΉ β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn) |
14 | 13 | adantr 482 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn) |
15 | | smodm 8298 |
. . 3
β’ (Smo
πΉ β Ord dom πΉ) |
16 | | ordin 6348 |
. . . . 5
β’ ((Ord
π΄ β§ Ord dom πΉ) β Ord (π΄ β© dom πΉ)) |
17 | | dmres 5960 |
. . . . . 6
β’ dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) |
18 | | ordeq 6325 |
. . . . . 6
β’ (dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) β (Ord dom (πΉ βΎ π΄) β Ord (π΄ β© dom πΉ))) |
19 | 17, 18 | ax-mp 5 |
. . . . 5
β’ (Ord dom
(πΉ βΎ π΄) β Ord (π΄ β© dom πΉ)) |
20 | 16, 19 | sylibr 233 |
. . . 4
β’ ((Ord
π΄ β§ Ord dom πΉ) β Ord dom (πΉ βΎ π΄)) |
21 | 20 | ancoms 460 |
. . 3
β’ ((Ord dom
πΉ β§ Ord π΄) β Ord dom (πΉ βΎ π΄)) |
22 | 15, 21 | sylan 581 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β Ord dom (πΉ βΎ π΄)) |
23 | | resss 5963 |
. . . . . 6
β’ (πΉ βΎ π΄) β πΉ |
24 | | dmss 5859 |
. . . . . 6
β’ ((πΉ βΎ π΄) β πΉ β dom (πΉ βΎ π΄) β dom πΉ) |
25 | 23, 24 | ax-mp 5 |
. . . . 5
β’ dom
(πΉ βΎ π΄) β dom πΉ |
26 | 1 | simp3bi 1148 |
. . . . 5
β’ (Smo
πΉ β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
27 | | ssralv 4011 |
. . . . 5
β’ (dom
(πΉ βΎ π΄) β dom πΉ β (βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
28 | 25, 26, 27 | mpsyl 68 |
. . . 4
β’ (Smo
πΉ β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
29 | 28 | adantr 482 |
. . 3
β’ ((Smo
πΉ β§ Ord π΄) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
30 | | ordtr1 6361 |
. . . . . . . . . . 11
β’ (Ord dom
(πΉ βΎ π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β dom (πΉ βΎ π΄))) |
31 | 22, 30 | syl 17 |
. . . . . . . . . 10
β’ ((Smo
πΉ β§ Ord π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β dom (πΉ βΎ π΄))) |
32 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (π΄ β© dom πΉ) β π΄ |
33 | 17, 32 | eqsstri 3979 |
. . . . . . . . . . 11
β’ dom
(πΉ βΎ π΄) β π΄ |
34 | 33 | sseli 3941 |
. . . . . . . . . 10
β’ (π¦ β dom (πΉ βΎ π΄) β π¦ β π΄) |
35 | 31, 34 | syl6 35 |
. . . . . . . . 9
β’ ((Smo
πΉ β§ Ord π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β π΄)) |
36 | 35 | expcomd 418 |
. . . . . . . 8
β’ ((Smo
πΉ β§ Ord π΄) β (π₯ β dom (πΉ βΎ π΄) β (π¦ β π₯ β π¦ β π΄))) |
37 | 36 | imp31 419 |
. . . . . . 7
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β π¦ β π΄) |
38 | 37 | fvresd 6863 |
. . . . . 6
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β ((πΉ βΎ π΄)βπ¦) = (πΉβπ¦)) |
39 | 33 | sseli 3941 |
. . . . . . . 8
β’ (π₯ β dom (πΉ βΎ π΄) β π₯ β π΄) |
40 | 39 | fvresd 6863 |
. . . . . . 7
β’ (π₯ β dom (πΉ βΎ π΄) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
41 | 40 | ad2antlr 726 |
. . . . . 6
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
42 | 38, 41 | eleq12d 2828 |
. . . . 5
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β (((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β (πΉβπ¦) β (πΉβπ₯))) |
43 | 42 | ralbidva 3169 |
. . . 4
β’ (((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β (βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
44 | 43 | ralbidva 3169 |
. . 3
β’ ((Smo
πΉ β§ Ord π΄) β (βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
45 | 29, 44 | mpbird 257 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯)) |
46 | | dfsmo2 8294 |
. 2
β’ (Smo
(πΉ βΎ π΄) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn β§ Ord dom (πΉ βΎ π΄) β§ βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯))) |
47 | 14, 22, 45, 46 | syl3anbrc 1344 |
1
β’ ((Smo
πΉ β§ Ord π΄) β Smo (πΉ βΎ π΄)) |