Step | Hyp | Ref
| Expression |
1 | | legso.l |
. . . . 5
β’ < = (( β€ βΎ
πΈ) β I
) |
2 | 1 | breqi 5154 |
. . . 4
β’ ((π΄ β π΅) < (πΆ β π·) β (π΄ β π΅)(( β€ βΎ πΈ) β I )(πΆ β π·)) |
3 | | brdif 5201 |
. . . 4
β’ ((π΄ β π΅)(( β€ βΎ πΈ) β I )(πΆ β π·) β ((π΄ β π΅)( β€ βΎ πΈ)(πΆ β π·) β§ Β¬ (π΄ β π΅) I (πΆ β π·))) |
4 | 2, 3 | bitri 275 |
. . 3
β’ ((π΄ β π΅) < (πΆ β π·) β ((π΄ β π΅)( β€ βΎ πΈ)(πΆ β π·) β§ Β¬ (π΄ β π΅) I (πΆ β π·))) |
5 | | ovex 7439 |
. . . . 5
β’ (πΆ β π·) β V |
6 | 5 | brresi 5989 |
. . . 4
β’ ((π΄ β π΅)( β€ βΎ πΈ)(πΆ β π·) β ((π΄ β π΅) β πΈ β§ (π΄ β π΅) β€ (πΆ β π·))) |
7 | 6 | anbi1i 625 |
. . 3
β’ (((π΄ β π΅)( β€ βΎ πΈ)(πΆ β π·) β§ Β¬ (π΄ β π΅) I (πΆ β π·)) β (((π΄ β π΅) β πΈ β§ (π΄ β π΅) β€ (πΆ β π·)) β§ Β¬ (π΄ β π΅) I (πΆ β π·))) |
8 | | an21 643 |
. . 3
β’ ((((π΄ β π΅) β πΈ β§ (π΄ β π΅) β€ (πΆ β π·)) β§ Β¬ (π΄ β π΅) I (πΆ β π·)) β ((π΄ β π΅) β€ (πΆ β π·) β§ ((π΄ β π΅) β πΈ β§ Β¬ (π΄ β π΅) I (πΆ β π·)))) |
9 | 4, 7, 8 | 3bitri 297 |
. 2
β’ ((π΄ β π΅) < (πΆ β π·) β ((π΄ β π΅) β€ (πΆ β π·) β§ ((π΄ β π΅) β πΈ β§ Β¬ (π΄ β π΅) I (πΆ β π·)))) |
10 | | ltgov.a |
. . . . . . 7
β’ (π β π΄ β π) |
11 | | ltgov.b |
. . . . . . 7
β’ (π β π΅ β π) |
12 | | legso.f |
. . . . . . 7
β’ (π β Fun β ) |
13 | | legso.d |
. . . . . . 7
β’ (π β (π Γ π) β dom β ) |
14 | 10, 11, 12, 13 | elovimad 7454 |
. . . . . 6
β’ (π β (π΄ β π΅) β ( β β (π Γ π))) |
15 | | legso.a |
. . . . . 6
β’ πΈ = ( β β (π Γ π)) |
16 | 14, 15 | eleqtrrdi 2845 |
. . . . 5
β’ (π β (π΄ β π΅) β πΈ) |
17 | 16 | biantrurd 534 |
. . . 4
β’ (π β (Β¬ (π΄ β π΅) I (πΆ β π·) β ((π΄ β π΅) β πΈ β§ Β¬ (π΄ β π΅) I (πΆ β π·)))) |
18 | 5 | ideq 5851 |
. . . . 5
β’ ((π΄ β π΅) I (πΆ β π·) β (π΄ β π΅) = (πΆ β π·)) |
19 | 18 | necon3bbii 2989 |
. . . 4
β’ (Β¬
(π΄ β π΅) I (πΆ β π·) β (π΄ β π΅) β (πΆ β π·)) |
20 | 17, 19 | bitr3di 286 |
. . 3
β’ (π β (((π΄ β π΅) β πΈ β§ Β¬ (π΄ β π΅) I (πΆ β π·)) β (π΄ β π΅) β (πΆ β π·))) |
21 | 20 | anbi2d 630 |
. 2
β’ (π β (((π΄ β π΅) β€ (πΆ β π·) β§ ((π΄ β π΅) β πΈ β§ Β¬ (π΄ β π΅) I (πΆ β π·))) β ((π΄ β π΅) β€ (πΆ β π·) β§ (π΄ β π΅) β (πΆ β π·)))) |
22 | 9, 21 | bitrid 283 |
1
β’ (π β ((π΄ β π΅) < (πΆ β π·) β ((π΄ β π΅) β€ (πΆ β π·) β§ (π΄ β π΅) β (πΆ β π·)))) |