Step | Hyp | Ref
| Expression |
1 | | df-smo 8350 |
. 2
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
2 | | ralcom 3284 |
. . . . . 6
β’
(βπ¦ β
dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) |
3 | | impexp 449 |
. . . . . . . . 9
β’ (((π¦ β dom πΉ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β (π¦ β dom πΉ β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
4 | | simpr 483 |
. . . . . . . . . . 11
β’ ((π¦ β dom πΉ β§ π¦ β π₯) β π¦ β π₯) |
5 | | ordtr1 6408 |
. . . . . . . . . . . . . . 15
β’ (Ord dom
πΉ β ((π¦ β π₯ β§ π₯ β dom πΉ) β π¦ β dom πΉ)) |
6 | 5 | 3impib 1114 |
. . . . . . . . . . . . . 14
β’ ((Ord dom
πΉ β§ π¦ β π₯ β§ π₯ β dom πΉ) β π¦ β dom πΉ) |
7 | 6 | 3com23 1124 |
. . . . . . . . . . . . 13
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β π¦ β dom πΉ) |
8 | | simp3 1136 |
. . . . . . . . . . . . 13
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β π¦ β π₯) |
9 | 7, 8 | jca 510 |
. . . . . . . . . . . 12
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β (π¦ β dom πΉ β§ π¦ β π₯)) |
10 | 9 | 3expia 1119 |
. . . . . . . . . . 11
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (π¦ β π₯ β (π¦ β dom πΉ β§ π¦ β π₯))) |
11 | 4, 10 | impbid2 225 |
. . . . . . . . . 10
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β ((π¦ β dom πΉ β§ π¦ β π₯) β π¦ β π₯)) |
12 | 11 | imbi1d 340 |
. . . . . . . . 9
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (((π¦ β dom πΉ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
13 | 3, 12 | bitr3id 284 |
. . . . . . . 8
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β ((π¦ β dom πΉ β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
14 | 13 | ralbidv2 3171 |
. . . . . . 7
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (βπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
15 | 14 | ralbidva 3173 |
. . . . . 6
β’ (Ord dom
πΉ β (βπ₯ β dom πΉβπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
16 | 2, 15 | bitrid 282 |
. . . . 5
β’ (Ord dom
πΉ β (βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
17 | 16 | pm5.32i 573 |
. . . 4
β’ ((Ord dom
πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
18 | 17 | anbi2i 621 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)))) |
19 | | 3anass 1093 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))))) |
20 | | 3anass 1093 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)))) |
21 | 18, 19, 20 | 3bitr4i 302 |
. 2
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
22 | 1, 21 | bitri 274 |
1
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |