Step | Hyp | Ref
| Expression |
1 | | frgrwopreg.a |
. . . . . 6
β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} |
2 | 1 | reqabi 3455 |
. . . . 5
β’ (π₯ β π΄ β (π₯ β π β§ (π·βπ₯) = πΎ)) |
3 | | fveqeq2 6901 |
. . . . . . 7
β’ (π₯ = π β ((π·βπ₯) = πΎ β (π·βπ) = πΎ)) |
4 | 3, 1 | elrab2 3687 |
. . . . . 6
β’ (π β π΄ β (π β π β§ (π·βπ) = πΎ)) |
5 | | eqtr3 2759 |
. . . . . . . . 9
β’ (((π·βπ) = πΎ β§ (π·βπ₯) = πΎ) β (π·βπ) = (π·βπ₯)) |
6 | 5 | expcom 415 |
. . . . . . . 8
β’ ((π·βπ₯) = πΎ β ((π·βπ) = πΎ β (π·βπ) = (π·βπ₯))) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ ((π₯ β π β§ (π·βπ₯) = πΎ) β ((π·βπ) = πΎ β (π·βπ) = (π·βπ₯))) |
8 | 7 | com12 32 |
. . . . . 6
β’ ((π·βπ) = πΎ β ((π₯ β π β§ (π·βπ₯) = πΎ) β (π·βπ) = (π·βπ₯))) |
9 | 4, 8 | simplbiim 506 |
. . . . 5
β’ (π β π΄ β ((π₯ β π β§ (π·βπ₯) = πΎ) β (π·βπ) = (π·βπ₯))) |
10 | 2, 9 | biimtrid 241 |
. . . 4
β’ (π β π΄ β (π₯ β π΄ β (π·βπ) = (π·βπ₯))) |
11 | 10 | imp 408 |
. . 3
β’ ((π β π΄ β§ π₯ β π΄) β (π·βπ) = (π·βπ₯)) |
12 | 11 | adantr 482 |
. 2
β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β (π·βπ) = (π·βπ₯)) |
13 | | frgrwopreg.v |
. . . 4
β’ π = (VtxβπΊ) |
14 | | frgrwopreg.d |
. . . 4
β’ π· = (VtxDegβπΊ) |
15 | | frgrwopreg.b |
. . . 4
β’ π΅ = (π β π΄) |
16 | 13, 14, 1, 15 | frgrwopreglem3 29567 |
. . 3
β’ ((π β π΄ β§ π β π΅) β (π·βπ) β (π·βπ)) |
17 | 16 | ad2ant2r 746 |
. 2
β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β (π·βπ) β (π·βπ)) |
18 | | fveqeq2 6901 |
. . . . . 6
β’ (π₯ = π§ β ((π·βπ₯) = πΎ β (π·βπ§) = πΎ)) |
19 | 18 | cbvrabv 3443 |
. . . . 5
β’ {π₯ β π β£ (π·βπ₯) = πΎ} = {π§ β π β£ (π·βπ§) = πΎ} |
20 | 1, 19 | eqtri 2761 |
. . . 4
β’ π΄ = {π§ β π β£ (π·βπ§) = πΎ} |
21 | 13, 14, 20, 15 | frgrwopreglem3 29567 |
. . 3
β’ ((π₯ β π΄ β§ π¦ β π΅) β (π·βπ₯) β (π·βπ¦)) |
22 | 21 | ad2ant2l 745 |
. 2
β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β (π·βπ₯) β (π·βπ¦)) |
23 | 12, 17, 22 | 3jca 1129 |
1
β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦))) |