| Step | Hyp | Ref
| Expression |
|---|
| 1 | | id 22 |
. . 3
β’ (πΊ β FriendGraph β πΊ β FriendGraph
) |
| 2 | | simpl 482 |
. . . 4
β’ ((π΄ β π β§ π β π) β π΄ β π) |
| 3 | | simpl 482 |
. . . 4
β’ ((π΅ β π β§ π β π) β π΅ β π) |
| 4 | 2, 3 | anim12i 612 |
. . 3
β’ (((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β (π΄ β π β§ π΅ β π)) |
| 5 | | simp2 1136 |
. . 3
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ΄) β (π·βπ΅)) |
| 6 | | frgrncvvdeq.v |
. . . 4
β’ π = (VtxβπΊ) |
| 7 | | frgrncvvdeq.d |
. . . 4
β’ π· = (VtxDegβπΊ) |
| 8 | | frgrwopreglem4a.e |
. . . 4
β’ πΈ = (EdgβπΊ) |
| 9 | 6, 7, 8 | frgrwopreglem4a 29831 |
. . 3
β’ ((πΊ β FriendGraph β§ (π΄ β π β§ π΅ β π) β§ (π·βπ΄) β (π·βπ΅)) β {π΄, π΅} β πΈ) |
| 10 | 1, 4, 5, 9 | syl3an 1159 |
. 2
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β {π΄, π΅} β πΈ) |
| 11 | | simpr 484 |
. . . 4
β’ ((π΄ β π β§ π β π) β π β π) |
| 12 | 11, 3 | anim12ci 613 |
. . 3
β’ (((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β (π΅ β π β§ π β π)) |
| 13 | | pm13.18 3021 |
. . . . 5
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅)) β (π·βπ) β (π·βπ΅)) |
| 14 | 13 | 3adant3 1131 |
. . . 4
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ) β (π·βπ΅)) |
| 15 | 14 | necomd 2995 |
. . 3
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ΅) β (π·βπ)) |
| 16 | 6, 7, 8 | frgrwopreglem4a 29831 |
. . 3
β’ ((πΊ β FriendGraph β§ (π΅ β π β§ π β π) β§ (π·βπ΅) β (π·βπ)) β {π΅, π} β πΈ) |
| 17 | 1, 12, 15, 16 | syl3an 1159 |
. 2
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β {π΅, π} β πΈ) |
| 18 | | simpr 484 |
. . . . 5
β’ ((π΅ β π β§ π β π) β π β π) |
| 19 | 11, 18 | anim12i 612 |
. . . 4
β’ (((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β (π β π β§ π β π)) |
| 20 | | simp3 1137 |
. . . 4
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ) β (π·βπ)) |
| 21 | 6, 7, 8 | frgrwopreglem4a 29831 |
. . . 4
β’ ((πΊ β FriendGraph β§ (π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β {π, π} β πΈ) |
| 22 | 1, 19, 20, 21 | syl3an 1159 |
. . 3
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β {π, π} β πΈ) |
| 23 | 2, 18 | anim12ci 613 |
. . . 4
β’ (((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β (π β π β§ π΄ β π)) |
| 24 | | pm13.181 3022 |
. . . . . 6
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ) β (π·βπ)) β (π·βπ΄) β (π·βπ)) |
| 25 | 24 | 3adant2 1130 |
. . . . 5
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ΄) β (π·βπ)) |
| 26 | 25 | necomd 2995 |
. . . 4
β’ (((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ)) β (π·βπ) β (π·βπ΄)) |
| 27 | 6, 7, 8 | frgrwopreglem4a 29831 |
. . . 4
β’ ((πΊ β FriendGraph β§ (π β π β§ π΄ β π) β§ (π·βπ) β (π·βπ΄)) β {π, π΄} β πΈ) |
| 28 | 1, 23, 26, 27 | syl3an 1159 |
. . 3
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β {π, π΄} β πΈ) |
| 29 | 22, 28 | jca 511 |
. 2
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β ({π, π} β πΈ β§ {π, π΄} β πΈ)) |
| 30 | 10, 17, 29 | jca31 514 |
1
β’ ((πΊ β FriendGraph β§
((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β (({π΄, π΅} β πΈ β§ {π΅, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π΄} β πΈ))) |
