Step | Hyp | Ref
| Expression |
1 | | funres 6544 |
. . . . . . . 8
β’ (Fun
π΄ β Fun (π΄ βΎ π΅)) |
2 | | funfn 6532 |
. . . . . . . 8
β’ (Fun
π΄ β π΄ Fn dom π΄) |
3 | | funfn 6532 |
. . . . . . . 8
β’ (Fun
(π΄ βΎ π΅) β (π΄ βΎ π΅) Fn dom (π΄ βΎ π΅)) |
4 | 1, 2, 3 | 3imtr3i 291 |
. . . . . . 7
β’ (π΄ Fn dom π΄ β (π΄ βΎ π΅) Fn dom (π΄ βΎ π΅)) |
5 | | resss 5963 |
. . . . . . . . 9
β’ (π΄ βΎ π΅) β π΄ |
6 | 5 | rnssi 5896 |
. . . . . . . 8
β’ ran
(π΄ βΎ π΅) β ran π΄ |
7 | | sstr 3953 |
. . . . . . . 8
β’ ((ran
(π΄ βΎ π΅) β ran π΄ β§ ran π΄ β On) β ran (π΄ βΎ π΅) β On) |
8 | 6, 7 | mpan 689 |
. . . . . . 7
β’ (ran
π΄ β On β ran
(π΄ βΎ π΅) β On) |
9 | 4, 8 | anim12i 614 |
. . . . . 6
β’ ((π΄ Fn dom π΄ β§ ran π΄ β On) β ((π΄ βΎ π΅) Fn dom (π΄ βΎ π΅) β§ ran (π΄ βΎ π΅) β On)) |
10 | | df-f 6501 |
. . . . . 6
β’ (π΄:dom π΄βΆOn β (π΄ Fn dom π΄ β§ ran π΄ β On)) |
11 | | df-f 6501 |
. . . . . 6
β’ ((π΄ βΎ π΅):dom (π΄ βΎ π΅)βΆOn β ((π΄ βΎ π΅) Fn dom (π΄ βΎ π΅) β§ ran (π΄ βΎ π΅) β On)) |
12 | 9, 10, 11 | 3imtr4i 292 |
. . . . 5
β’ (π΄:dom π΄βΆOn β (π΄ βΎ π΅):dom (π΄ βΎ π΅)βΆOn) |
13 | 12 | a1i 11 |
. . . 4
β’ (π΅ β dom π΄ β (π΄:dom π΄βΆOn β (π΄ βΎ π΅):dom (π΄ βΎ π΅)βΆOn)) |
14 | | ordelord 6340 |
. . . . . . 7
β’ ((Ord dom
π΄ β§ π΅ β dom π΄) β Ord π΅) |
15 | 14 | expcom 415 |
. . . . . 6
β’ (π΅ β dom π΄ β (Ord dom π΄ β Ord π΅)) |
16 | | ordin 6348 |
. . . . . . 7
β’ ((Ord
π΅ β§ Ord dom π΄) β Ord (π΅ β© dom π΄)) |
17 | 16 | ex 414 |
. . . . . 6
β’ (Ord
π΅ β (Ord dom π΄ β Ord (π΅ β© dom π΄))) |
18 | 15, 17 | syli 39 |
. . . . 5
β’ (π΅ β dom π΄ β (Ord dom π΄ β Ord (π΅ β© dom π΄))) |
19 | | dmres 5960 |
. . . . . 6
β’ dom
(π΄ βΎ π΅) = (π΅ β© dom π΄) |
20 | | ordeq 6325 |
. . . . . 6
β’ (dom
(π΄ βΎ π΅) = (π΅ β© dom π΄) β (Ord dom (π΄ βΎ π΅) β Ord (π΅ β© dom π΄))) |
21 | 19, 20 | ax-mp 5 |
. . . . 5
β’ (Ord dom
(π΄ βΎ π΅) β Ord (π΅ β© dom π΄)) |
22 | 18, 21 | syl6ibr 252 |
. . . 4
β’ (π΅ β dom π΄ β (Ord dom π΄ β Ord dom (π΄ βΎ π΅))) |
23 | | dmss 5859 |
. . . . . . . . 9
β’ ((π΄ βΎ π΅) β π΄ β dom (π΄ βΎ π΅) β dom π΄) |
24 | 5, 23 | ax-mp 5 |
. . . . . . . 8
β’ dom
(π΄ βΎ π΅) β dom π΄ |
25 | | ssralv 4011 |
. . . . . . . 8
β’ (dom
(π΄ βΎ π΅) β dom π΄ β (βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
26 | 24, 25 | ax-mp 5 |
. . . . . . 7
β’
(βπ₯ β
dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
27 | | ssralv 4011 |
. . . . . . . . 9
β’ (dom
(π΄ βΎ π΅) β dom π΄ β (βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
28 | 24, 27 | ax-mp 5 |
. . . . . . . 8
β’
(βπ¦ β
dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
29 | 28 | ralimi 3083 |
. . . . . . 7
β’
(βπ₯ β
dom (π΄ βΎ π΅)βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
30 | 26, 29 | syl 17 |
. . . . . 6
β’
(βπ₯ β
dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
31 | | inss1 4189 |
. . . . . . . . . . . . 13
β’ (π΅ β© dom π΄) β π΅ |
32 | 19, 31 | eqsstri 3979 |
. . . . . . . . . . . 12
β’ dom
(π΄ βΎ π΅) β π΅ |
33 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β π₯ β dom (π΄ βΎ π΅)) |
34 | 32, 33 | sselid 3943 |
. . . . . . . . . . 11
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β π₯ β π΅) |
35 | 34 | fvresd 6863 |
. . . . . . . . . 10
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β ((π΄ βΎ π΅)βπ₯) = (π΄βπ₯)) |
36 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β π¦ β dom (π΄ βΎ π΅)) |
37 | 32, 36 | sselid 3943 |
. . . . . . . . . . 11
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β π¦ β π΅) |
38 | 37 | fvresd 6863 |
. . . . . . . . . 10
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β ((π΄ βΎ π΅)βπ¦) = (π΄βπ¦)) |
39 | 35, 38 | eleq12d 2828 |
. . . . . . . . 9
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β (((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦) β (π΄βπ₯) β (π΄βπ¦))) |
40 | 39 | imbi2d 341 |
. . . . . . . 8
β’ ((π₯ β dom (π΄ βΎ π΅) β§ π¦ β dom (π΄ βΎ π΅)) β ((π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦)) β (π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
41 | 40 | ralbidva 3169 |
. . . . . . 7
β’ (π₯ β dom (π΄ βΎ π΅) β (βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦)) β βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
42 | 41 | ralbiia 3091 |
. . . . . 6
β’
(βπ₯ β
dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) |
43 | 30, 42 | sylibr 233 |
. . . . 5
β’
(βπ₯ β
dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦))) |
44 | 43 | a1i 11 |
. . . 4
β’ (π΅ β dom π΄ β (βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦)))) |
45 | 13, 22, 44 | 3anim123d 1444 |
. . 3
β’ (π΅ β dom π΄ β ((π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) β ((π΄ βΎ π΅):dom (π΄ βΎ π΅)βΆOn β§ Ord dom (π΄ βΎ π΅) β§ βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦))))) |
46 | | df-smo 8293 |
. . 3
β’ (Smo
π΄ β (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
47 | | df-smo 8293 |
. . 3
β’ (Smo
(π΄ βΎ π΅) β ((π΄ βΎ π΅):dom (π΄ βΎ π΅)βΆOn β§ Ord dom (π΄ βΎ π΅) β§ βπ₯ β dom (π΄ βΎ π΅)βπ¦ β dom (π΄ βΎ π΅)(π₯ β π¦ β ((π΄ βΎ π΅)βπ₯) β ((π΄ βΎ π΅)βπ¦)))) |
48 | 45, 46, 47 | 3imtr4g 296 |
. 2
β’ (π΅ β dom π΄ β (Smo π΄ β Smo (π΄ βΎ π΅))) |
49 | 48 | impcom 409 |
1
β’ ((Smo
π΄ β§ π΅ β dom π΄) β Smo (π΄ βΎ π΅)) |