Step | Hyp | Ref
| Expression |
1 | | df-smo 8346 |
. 2
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
2 | | ralcom 3287 |
. . . . . 6
β’
(βπ¦ β
dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) |
3 | | impexp 452 |
. . . . . . . . 9
β’ (((π¦ β dom πΉ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β (π¦ β dom πΉ β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
4 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π¦ β dom πΉ β§ π¦ β π₯) β π¦ β π₯) |
5 | | ordtr1 6408 |
. . . . . . . . . . . . . . 15
β’ (Ord dom
πΉ β ((π¦ β π₯ β§ π₯ β dom πΉ) β π¦ β dom πΉ)) |
6 | 5 | 3impib 1117 |
. . . . . . . . . . . . . 14
β’ ((Ord dom
πΉ β§ π¦ β π₯ β§ π₯ β dom πΉ) β π¦ β dom πΉ) |
7 | 6 | 3com23 1127 |
. . . . . . . . . . . . 13
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β π¦ β dom πΉ) |
8 | | simp3 1139 |
. . . . . . . . . . . . 13
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β π¦ β π₯) |
9 | 7, 8 | jca 513 |
. . . . . . . . . . . 12
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ β§ π¦ β π₯) β (π¦ β dom πΉ β§ π¦ β π₯)) |
10 | 9 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (π¦ β π₯ β (π¦ β dom πΉ β§ π¦ β π₯))) |
11 | 4, 10 | impbid2 225 |
. . . . . . . . . 10
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β ((π¦ β dom πΉ β§ π¦ β π₯) β π¦ β π₯)) |
12 | 11 | imbi1d 342 |
. . . . . . . . 9
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (((π¦ β dom πΉ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
13 | 3, 12 | bitr3id 285 |
. . . . . . . 8
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β ((π¦ β dom πΉ β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) |
14 | 13 | ralbidv2 3174 |
. . . . . . 7
β’ ((Ord dom
πΉ β§ π₯ β dom πΉ) β (βπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
15 | 14 | ralbidva 3176 |
. . . . . 6
β’ (Ord dom
πΉ β (βπ₯ β dom πΉβπ¦ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
16 | 2, 15 | bitrid 283 |
. . . . 5
β’ (Ord dom
πΉ β (βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)) β βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
17 | 16 | pm5.32i 576 |
. . . 4
β’ ((Ord dom
πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
18 | 17 | anbi2i 624 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯)))) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)))) |
19 | | 3anass 1096 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))))) |
20 | | 3anass 1096 |
. . 3
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)) β (πΉ:dom πΉβΆOn β§ (Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯)))) |
21 | 18, 19, 20 | 3bitr4i 303 |
. 2
β’ ((πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ¦ β dom πΉβπ₯ β dom πΉ(π¦ β π₯ β (πΉβπ¦) β (πΉβπ₯))) β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |
22 | 1, 21 | bitri 275 |
1
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β π₯ (πΉβπ¦) β (πΉβπ₯))) |