Step | Hyp | Ref
| Expression |
1 | | smodm 8298 |
. . . . 5
β’ (Smo
π΅ β Ord dom π΅) |
2 | | ordtr1 6361 |
. . . . . . 7
β’ (Ord dom
π΅ β ((πΆ β π΄ β§ π΄ β dom π΅) β πΆ β dom π΅)) |
3 | 2 | ancomsd 467 |
. . . . . 6
β’ (Ord dom
π΅ β ((π΄ β dom π΅ β§ πΆ β π΄) β πΆ β dom π΅)) |
4 | 3 | expdimp 454 |
. . . . 5
β’ ((Ord dom
π΅ β§ π΄ β dom π΅) β (πΆ β π΄ β πΆ β dom π΅)) |
5 | 1, 4 | sylan 581 |
. . . 4
β’ ((Smo
π΅ β§ π΄ β dom π΅) β (πΆ β π΄ β πΆ β dom π΅)) |
6 | | df-smo 8293 |
. . . . . 6
β’ (Smo
π΅ β (π΅:dom π΅βΆOn β§ Ord dom π΅ β§ βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
7 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π₯ = πΆ β (π₯ β π¦ β πΆ β π¦)) |
8 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = πΆ β (π΅βπ₯) = (π΅βπΆ)) |
9 | 8 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ = πΆ β ((π΅βπ₯) β (π΅βπ¦) β (π΅βπΆ) β (π΅βπ¦))) |
10 | 7, 9 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = πΆ β ((π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β (πΆ β π¦ β (π΅βπΆ) β (π΅βπ¦)))) |
11 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (πΆ β π¦ β πΆ β π΄)) |
12 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (π΅βπ¦) = (π΅βπ΄)) |
13 | 12 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β ((π΅βπΆ) β (π΅βπ¦) β (π΅βπΆ) β (π΅βπ΄))) |
14 | 11, 13 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = π΄ β ((πΆ β π¦ β (π΅βπΆ) β (π΅βπ¦)) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
15 | 10, 14 | rspc2v 3589 |
. . . . . . . . 9
β’ ((πΆ β dom π΅ β§ π΄ β dom π΅) β (βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
16 | 15 | ancoms 460 |
. . . . . . . 8
β’ ((π΄ β dom π΅ β§ πΆ β dom π΅) β (βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
17 | 16 | com12 32 |
. . . . . . 7
β’
(βπ₯ β
dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β ((π΄ β dom π΅ β§ πΆ β dom π΅) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
18 | 17 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π΅:dom π΅βΆOn β§ Ord dom π΅ β§ βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦))) β ((π΄ β dom π΅ β§ πΆ β dom π΅) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
19 | 6, 18 | sylbi 216 |
. . . . 5
β’ (Smo
π΅ β ((π΄ β dom π΅ β§ πΆ β dom π΅) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
20 | 19 | expdimp 454 |
. . . 4
β’ ((Smo
π΅ β§ π΄ β dom π΅) β (πΆ β dom π΅ β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
21 | 5, 20 | syld 47 |
. . 3
β’ ((Smo
π΅ β§ π΄ β dom π΅) β (πΆ β π΄ β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄)))) |
22 | 21 | pm2.43d 53 |
. 2
β’ ((Smo
π΅ β§ π΄ β dom π΅) β (πΆ β π΄ β (π΅βπΆ) β (π΅βπ΄))) |
23 | 22 | 3impia 1118 |
1
β’ ((Smo
π΅ β§ π΄ β dom π΅ β§ πΆ β π΄) β (π΅βπΆ) β (π΅βπ΄)) |