Step | Hyp | Ref
| Expression |
1 | | simplrr 775 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΄ β π΅) β π΅ β Ο) |
2 | | simplrl 774 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΄ β π΅) β π΄ β Ο) |
3 | | simpr 484 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΄ β π΅) β π΄ β π΅) |
4 | | simplll 772 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΄ β π΅) β π) |
5 | | incom 4196 |
. . . 4
β’ (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = (((πΉβπ΅) β (πΉβsuc π΅)) β© ((πΉβπ΄) β (πΉβsuc π΄))) |
6 | | isf32lem.a |
. . . . 5
β’ (π β πΉ:ΟβΆπ« πΊ) |
7 | | isf32lem.b |
. . . . 5
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
8 | | isf32lem.c |
. . . . 5
β’ (π β Β¬ β© ran πΉ β ran πΉ) |
9 | 6, 7, 8 | isf32lem3 10352 |
. . . 4
β’ (((π΅ β Ο β§ π΄ β Ο) β§ (π΄ β π΅ β§ π)) β (((πΉβπ΅) β (πΉβsuc π΅)) β© ((πΉβπ΄) β (πΉβsuc π΄))) = β
) |
10 | 5, 9 | eqtrid 2778 |
. . 3
β’ (((π΅ β Ο β§ π΄ β Ο) β§ (π΄ β π΅ β§ π)) β (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = β
) |
11 | 1, 2, 3, 4, 10 | syl22anc 836 |
. 2
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΄ β π΅) β (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = β
) |
12 | | simplrl 774 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΅ β π΄) β π΄ β Ο) |
13 | | simplrr 775 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΅ β π΄) β π΅ β Ο) |
14 | | simpr 484 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΅ β π΄) β π΅ β π΄) |
15 | | simplll 772 |
. . 3
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΅ β π΄) β π) |
16 | 6, 7, 8 | isf32lem3 10352 |
. . 3
β’ (((π΄ β Ο β§ π΅ β Ο) β§ (π΅ β π΄ β§ π)) β (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = β
) |
17 | 12, 13, 14, 15, 16 | syl22anc 836 |
. 2
β’ ((((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β§ π΅ β π΄) β (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = β
) |
18 | | simplr 766 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β π΄ β π΅) |
19 | | nnord 7860 |
. . . . . 6
β’ (π΄ β Ο β Ord π΄) |
20 | | nnord 7860 |
. . . . . 6
β’ (π΅ β Ο β Ord π΅) |
21 | | ordtri3 6394 |
. . . . . 6
β’ ((Ord
π΄ β§ Ord π΅) β (π΄ = π΅ β Β¬ (π΄ β π΅ β¨ π΅ β π΄))) |
22 | 19, 20, 21 | syl2an 595 |
. . . . 5
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ = π΅ β Β¬ (π΄ β π΅ β¨ π΅ β π΄))) |
23 | 22 | adantl 481 |
. . . 4
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π΄ = π΅ β Β¬ (π΄ β π΅ β¨ π΅ β π΄))) |
24 | 23 | necon2abid 2977 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((π΄ β π΅ β¨ π΅ β π΄) β π΄ β π΅)) |
25 | 18, 24 | mpbird 257 |
. 2
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π΄ β π΅ β¨ π΅ β π΄)) |
26 | 11, 17, 25 | mpjaodan 955 |
1
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((πΉβπ΄) β (πΉβsuc π΄)) β© ((πΉβπ΅) β (πΉβsuc π΅))) = β
) |