Step | Hyp | Ref
| Expression |
1 | | dfsmo2 6290 |
. . . . . . 7
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
2 | 1 | simp1bi 1012 |
. . . . . 6
β’ (Smo
πΉ β πΉ:dom πΉβΆOn) |
3 | | ffun 5370 |
. . . . . 6
β’ (πΉ:dom πΉβΆOn β Fun πΉ) |
4 | 2, 3 | syl 14 |
. . . . 5
β’ (Smo
πΉ β Fun πΉ) |
5 | | funres 5259 |
. . . . . 6
β’ (Fun
πΉ β Fun (πΉ βΎ π΄)) |
6 | | funfn 5248 |
. . . . . 6
β’ (Fun
(πΉ βΎ π΄) β (πΉ βΎ π΄) Fn dom (πΉ βΎ π΄)) |
7 | 5, 6 | sylib 122 |
. . . . 5
β’ (Fun
πΉ β (πΉ βΎ π΄) Fn dom (πΉ βΎ π΄)) |
8 | 4, 7 | syl 14 |
. . . 4
β’ (Smo
πΉ β (πΉ βΎ π΄) Fn dom (πΉ βΎ π΄)) |
9 | | df-ima 4641 |
. . . . . 6
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
10 | | imassrn 4983 |
. . . . . 6
β’ (πΉ β π΄) β ran πΉ |
11 | 9, 10 | eqsstrri 3190 |
. . . . 5
β’ ran
(πΉ βΎ π΄) β ran πΉ |
12 | | frn 5376 |
. . . . . 6
β’ (πΉ:dom πΉβΆOn β ran πΉ β On) |
13 | 2, 12 | syl 14 |
. . . . 5
β’ (Smo
πΉ β ran πΉ β On) |
14 | 11, 13 | sstrid 3168 |
. . . 4
β’ (Smo
πΉ β ran (πΉ βΎ π΄) β On) |
15 | | df-f 5222 |
. . . 4
β’ ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn β ((πΉ βΎ π΄) Fn dom (πΉ βΎ π΄) β§ ran (πΉ βΎ π΄) β On)) |
16 | 8, 14, 15 | sylanbrc 417 |
. . 3
β’ (Smo
πΉ β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn) |
17 | 16 | adantr 276 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn) |
18 | | smodm 6294 |
. . 3
β’ (Smo
πΉ β Ord dom πΉ) |
19 | | ordin 4387 |
. . . . 5
β’ ((Ord
π΄ β§ Ord dom πΉ) β Ord (π΄ β© dom πΉ)) |
20 | | dmres 4930 |
. . . . . 6
β’ dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) |
21 | | ordeq 4374 |
. . . . . 6
β’ (dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) β (Ord dom (πΉ βΎ π΄) β Ord (π΄ β© dom πΉ))) |
22 | 20, 21 | ax-mp 5 |
. . . . 5
β’ (Ord dom
(πΉ βΎ π΄) β Ord (π΄ β© dom πΉ)) |
23 | 19, 22 | sylibr 134 |
. . . 4
β’ ((Ord
π΄ β§ Ord dom πΉ) β Ord dom (πΉ βΎ π΄)) |
24 | 23 | ancoms 268 |
. . 3
β’ ((Ord dom
πΉ β§ Ord π΄) β Ord dom (πΉ βΎ π΄)) |
25 | 18, 24 | sylan 283 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β Ord dom (πΉ βΎ π΄)) |
26 | | resss 4933 |
. . . . . 6
β’ (πΉ βΎ π΄) β πΉ |
27 | | dmss 4828 |
. . . . . 6
β’ ((πΉ βΎ π΄) β πΉ β dom (πΉ βΎ π΄) β dom πΉ) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
β’ dom
(πΉ βΎ π΄) β dom πΉ |
29 | 1 | simp3bi 1014 |
. . . . 5
β’ (Smo
πΉ β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
30 | | ssralv 3221 |
. . . . 5
β’ (dom
(πΉ βΎ π΄) β dom πΉ β (βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
31 | 28, 29, 30 | mpsyl 65 |
. . . 4
β’ (Smo
πΉ β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
32 | 31 | adantr 276 |
. . 3
β’ ((Smo
πΉ β§ Ord π΄) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) |
33 | | ordtr1 4390 |
. . . . . . . . . . 11
β’ (Ord dom
(πΉ βΎ π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β dom (πΉ βΎ π΄))) |
34 | 25, 33 | syl 14 |
. . . . . . . . . 10
β’ ((Smo
πΉ β§ Ord π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β dom (πΉ βΎ π΄))) |
35 | | inss1 3357 |
. . . . . . . . . . . 12
β’ (π΄ β© dom πΉ) β π΄ |
36 | 20, 35 | eqsstri 3189 |
. . . . . . . . . . 11
β’ dom
(πΉ βΎ π΄) β π΄ |
37 | 36 | sseli 3153 |
. . . . . . . . . 10
β’ (π¦ β dom (πΉ βΎ π΄) β π¦ β π΄) |
38 | 34, 37 | syl6 33 |
. . . . . . . . 9
β’ ((Smo
πΉ β§ Ord π΄) β ((π¦ β π₯ β§ π₯ β dom (πΉ βΎ π΄)) β π¦ β π΄)) |
39 | 38 | expcomd 1441 |
. . . . . . . 8
β’ ((Smo
πΉ β§ Ord π΄) β (π₯ β dom (πΉ βΎ π΄) β (π¦ β π₯ β π¦ β π΄))) |
40 | 39 | imp31 256 |
. . . . . . 7
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β π¦ β π΄) |
41 | | fvres 5541 |
. . . . . . 7
β’ (π¦ β π΄ β ((πΉ βΎ π΄)βπ¦) = (πΉβπ¦)) |
42 | 40, 41 | syl 14 |
. . . . . 6
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β ((πΉ βΎ π΄)βπ¦) = (πΉβπ¦)) |
43 | 36 | sseli 3153 |
. . . . . . . 8
β’ (π₯ β dom (πΉ βΎ π΄) β π₯ β π΄) |
44 | | fvres 5541 |
. . . . . . . 8
β’ (π₯ β π΄ β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
45 | 43, 44 | syl 14 |
. . . . . . 7
β’ (π₯ β dom (πΉ βΎ π΄) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
46 | 45 | ad2antlr 489 |
. . . . . 6
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
47 | 42, 46 | eleq12d 2248 |
. . . . 5
β’ ((((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β§ π¦ β π₯) β (((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β (πΉβπ¦) β (πΉβπ₯))) |
48 | 47 | ralbidva 2473 |
. . . 4
β’ (((Smo
πΉ β§ Ord π΄) β§ π₯ β dom (πΉ βΎ π΄)) β (βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
49 | 48 | ralbidva 2473 |
. . 3
β’ ((Smo
πΉ β§ Ord π΄) β (βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
50 | 32, 49 | mpbird 167 |
. 2
β’ ((Smo
πΉ β§ Ord π΄) β βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯)) |
51 | | dfsmo2 6290 |
. 2
β’ (Smo
(πΉ βΎ π΄) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆOn β§ Ord dom (πΉ βΎ π΄) β§ βπ₯ β dom (πΉ βΎ π΄)βπ¦ β π₯ ((πΉ βΎ π΄)βπ¦) β ((πΉ βΎ π΄)βπ₯))) |
52 | 17, 25, 50, 51 | syl3anbrc 1181 |
1
β’ ((Smo
πΉ β§ Ord π΄) β Smo (πΉ βΎ π΄)) |