Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . 5
β’ (π = π΅ β (πΉβπ) = (πΉβπ΅)) |
2 | 1 | sseq1d 4013 |
. . . 4
β’ (π = π΅ β ((πΉβπ) β (πΉβπ΅) β (πΉβπ΅) β (πΉβπ΅))) |
3 | 2 | imbi2d 340 |
. . 3
β’ (π = π΅ β ((π β (πΉβπ) β (πΉβπ΅)) β (π β (πΉβπ΅) β (πΉβπ΅)))) |
4 | | fveq2 6891 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
5 | 4 | sseq1d 4013 |
. . . 4
β’ (π = π β ((πΉβπ) β (πΉβπ΅) β (πΉβπ) β (πΉβπ΅))) |
6 | 5 | imbi2d 340 |
. . 3
β’ (π = π β ((π β (πΉβπ) β (πΉβπ΅)) β (π β (πΉβπ) β (πΉβπ΅)))) |
7 | | fveq2 6891 |
. . . . 5
β’ (π = suc π β (πΉβπ) = (πΉβsuc π)) |
8 | 7 | sseq1d 4013 |
. . . 4
β’ (π = suc π β ((πΉβπ) β (πΉβπ΅) β (πΉβsuc π) β (πΉβπ΅))) |
9 | 8 | imbi2d 340 |
. . 3
β’ (π = suc π β ((π β (πΉβπ) β (πΉβπ΅)) β (π β (πΉβsuc π) β (πΉβπ΅)))) |
10 | | fveq2 6891 |
. . . . 5
β’ (π = π΄ β (πΉβπ) = (πΉβπ΄)) |
11 | 10 | sseq1d 4013 |
. . . 4
β’ (π = π΄ β ((πΉβπ) β (πΉβπ΅) β (πΉβπ΄) β (πΉβπ΅))) |
12 | 11 | imbi2d 340 |
. . 3
β’ (π = π΄ β ((π β (πΉβπ) β (πΉβπ΅)) β (π β (πΉβπ΄) β (πΉβπ΅)))) |
13 | | ssid 4004 |
. . . 4
β’ (πΉβπ΅) β (πΉβπ΅) |
14 | 13 | 2a1i 12 |
. . 3
β’ (π΅ β Ο β (π β (πΉβπ΅) β (πΉβπ΅))) |
15 | | isf32lem.b |
. . . . . . 7
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
16 | | suceq 6430 |
. . . . . . . . . 10
β’ (π₯ = π β suc π₯ = suc π) |
17 | 16 | fveq2d 6895 |
. . . . . . . . 9
β’ (π₯ = π β (πΉβsuc π₯) = (πΉβsuc π)) |
18 | | fveq2 6891 |
. . . . . . . . 9
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
19 | 17, 18 | sseq12d 4015 |
. . . . . . . 8
β’ (π₯ = π β ((πΉβsuc π₯) β (πΉβπ₯) β (πΉβsuc π) β (πΉβπ))) |
20 | 19 | rspcv 3608 |
. . . . . . 7
β’ (π β Ο β
(βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯) β (πΉβsuc π) β (πΉβπ))) |
21 | 15, 20 | syl5 34 |
. . . . . 6
β’ (π β Ο β (π β (πΉβsuc π) β (πΉβπ))) |
22 | 21 | ad2antrr 724 |
. . . . 5
β’ (((π β Ο β§ π΅ β Ο) β§ π΅ β π) β (π β (πΉβsuc π) β (πΉβπ))) |
23 | | sstr2 3989 |
. . . . 5
β’ ((πΉβsuc π) β (πΉβπ) β ((πΉβπ) β (πΉβπ΅) β (πΉβsuc π) β (πΉβπ΅))) |
24 | 22, 23 | syl6 35 |
. . . 4
β’ (((π β Ο β§ π΅ β Ο) β§ π΅ β π) β (π β ((πΉβπ) β (πΉβπ΅) β (πΉβsuc π) β (πΉβπ΅)))) |
25 | 24 | a2d 29 |
. . 3
β’ (((π β Ο β§ π΅ β Ο) β§ π΅ β π) β ((π β (πΉβπ) β (πΉβπ΅)) β (π β (πΉβsuc π) β (πΉβπ΅)))) |
26 | 3, 6, 9, 12, 14, 25 | findsg 7892 |
. 2
β’ (((π΄ β Ο β§ π΅ β Ο) β§ π΅ β π΄) β (π β (πΉβπ΄) β (πΉβπ΅))) |
27 | 26 | impr 455 |
1
β’ (((π΄ β Ο β§ π΅ β Ο) β§ (π΅ β π΄ β§ π)) β (πΉβπ΄) β (πΉβπ΅)) |