Step | Hyp | Ref
| Expression |
1 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β π β π₯) |
2 | 1 | anim1i 616 |
. . . . . . . . . . . . 13
β’
(((((πΊ β
FriendGraph β§ π β
π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ π β π¦) β (π β π₯ β§ π β π¦)) |
3 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β πΊ β FriendGraph ) |
4 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ((π·βπ₯) = πΎ β (π·βπ) = πΎ)) |
5 | | frgrwopreg.a |
. . . . . . . . . . . . . . . . . . . . 21
β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} |
6 | 4, 5 | elrab2 3653 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β (π β π β§ (π·βπ) = πΎ)) |
7 | 6 | simplbi 499 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β π β π) |
8 | | rabidim1 3431 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β {π₯ β π β£ (π·βπ₯) = πΎ} β π₯ β π) |
9 | 8, 5 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΄ β π₯ β π) |
10 | 7, 9 | anim12i 614 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π΄ β§ π₯ β π΄) β (π β π β§ π₯ β π)) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β (π β π β§ π₯ β π)) |
12 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β π΄) β π β π) |
13 | | frgrwopreg.b |
. . . . . . . . . . . . . . . . . . 19
β’ π΅ = (π β π΄) |
14 | 12, 13 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β π β π) |
15 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (π β π΄) β π¦ β π) |
16 | 15, 13 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π΅ β π¦ β π) |
17 | 14, 16 | anim12i 614 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π΅ β§ π¦ β π΅) β (π β π β§ π¦ β π)) |
18 | 11, 17 | anim12i 614 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β ((π β π β§ π₯ β π) β§ (π β π β§ π¦ β π))) |
19 | | frgrwopreg.v |
. . . . . . . . . . . . . . . . . 18
β’ π = (VtxβπΊ) |
20 | | frgrwopreg.d |
. . . . . . . . . . . . . . . . . 18
β’ π· = (VtxDegβπΊ) |
21 | | frgrwopreg.e |
. . . . . . . . . . . . . . . . . 18
β’ πΈ = (EdgβπΊ) |
22 | 19, 20, 5, 13, 21 | frgrwopreglem5lem 29306 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦))) |
23 | 22 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦))) |
24 | 3, 18, 23 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β (πΊ β FriendGraph β§ ((π β π β§ π₯ β π) β§ (π β π β§ π¦ β π)) β§ ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦)))) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((πΊ β
FriendGraph β§ π β
π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ π β π¦) β (πΊ β FriendGraph β§ ((π β π β§ π₯ β π) β§ (π β π β§ π¦ β π)) β§ ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦)))) |
26 | 19, 20, 21 | frgrwopreglem5a 29297 |
. . . . . . . . . . . . . 14
β’ ((πΊ β FriendGraph β§
((π β π β§ π₯ β π) β§ (π β π β§ π¦ β π)) β§ ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦))) β (({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((πΊ β
FriendGraph β§ π β
π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ π β π¦) β (({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) |
28 | | 3anass 1096 |
. . . . . . . . . . . . 13
β’ (((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)) β ((π β π₯ β§ π β π¦) β§ (({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
29 | 2, 27, 28 | sylanbrc 584 |
. . . . . . . . . . . 12
β’
(((((πΊ β
FriendGraph β§ π β
π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ π β π¦) β ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) |
30 | 29 | ex 414 |
. . . . . . . . . . 11
β’ ((((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β (π β π¦ β ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
31 | 30 | reximdvva 3203 |
. . . . . . . . . 10
β’ (((πΊ β FriendGraph β§ π β π₯) β§ (π β π΄ β§ π₯ β π΄)) β (βπ β π΅ βπ¦ β π΅ π β π¦ β βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
32 | 31 | exp31 421 |
. . . . . . . . 9
β’ (πΊ β FriendGraph β
(π β π₯ β ((π β π΄ β§ π₯ β π΄) β (βπ β π΅ βπ¦ β π΅ π β π¦ β βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))))) |
33 | 32 | com24 95 |
. . . . . . . 8
β’ (πΊ β FriendGraph β
(βπ β π΅ βπ¦ β π΅ π β π¦ β ((π β π΄ β§ π₯ β π΄) β (π β π₯ β βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))))) |
34 | 33 | imp31 419 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§
βπ β π΅ βπ¦ β π΅ π β π¦) β§ (π β π΄ β§ π₯ β π΄)) β (π β π₯ β βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
35 | 34 | reximdvva 3203 |
. . . . . 6
β’ ((πΊ β FriendGraph β§
βπ β π΅ βπ¦ β π΅ π β π¦) β (βπ β π΄ βπ₯ β π΄ π β π₯ β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
36 | 35 | ex 414 |
. . . . 5
β’ (πΊ β FriendGraph β
(βπ β π΅ βπ¦ β π΅ π β π¦ β (βπ β π΄ βπ₯ β π΄ π β π₯ β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))))) |
37 | 36 | com13 88 |
. . . 4
β’
(βπ β
π΄ βπ₯ β π΄ π β π₯ β (βπ β π΅ βπ¦ β π΅ π β π¦ β (πΊ β FriendGraph β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))))) |
38 | 37 | imp 408 |
. . 3
β’
((βπ β
π΄ βπ₯ β π΄ π β π₯ β§ βπ β π΅ βπ¦ β π΅ π β π¦) β (πΊ β FriendGraph β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
39 | 19, 20, 5, 13 | frgrwopreglem1 29298 |
. . . 4
β’ (π΄ β V β§ π΅ β V) |
40 | | hashgt12el 14329 |
. . . . . 6
β’ ((π΄ β V β§ 1 <
(β―βπ΄)) β
βπ β π΄ βπ₯ β π΄ π β π₯) |
41 | 40 | ex 414 |
. . . . 5
β’ (π΄ β V β (1 <
(β―βπ΄) β
βπ β π΄ βπ₯ β π΄ π β π₯)) |
42 | | hashgt12el 14329 |
. . . . . 6
β’ ((π΅ β V β§ 1 <
(β―βπ΅)) β
βπ β π΅ βπ¦ β π΅ π β π¦) |
43 | 42 | ex 414 |
. . . . 5
β’ (π΅ β V β (1 <
(β―βπ΅) β
βπ β π΅ βπ¦ β π΅ π β π¦)) |
44 | 41, 43 | im2anan9 621 |
. . . 4
β’ ((π΄ β V β§ π΅ β V) β ((1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β (βπ β
π΄ βπ₯ β π΄ π β π₯ β§ βπ β π΅ βπ¦ β π΅ π β π¦))) |
45 | 39, 44 | ax-mp 5 |
. . 3
β’ ((1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β (βπ β
π΄ βπ₯ β π΄ π β π₯ β§ βπ β π΅ βπ¦ β π΅ π β π¦)) |
46 | 38, 45 | syl11 33 |
. 2
β’ (πΊ β FriendGraph β ((1
< (β―βπ΄)
β§ 1 < (β―βπ΅)) β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ)))) |
47 | 46 | 3impib 1117 |
1
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β βπ β
π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) |