Step | Hyp | Ref
| Expression |
1 | | frgrwopreg.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | frgrwopreg.d |
. . 3
β’ π· = (VtxDegβπΊ) |
3 | | frgrwopreg.a |
. . 3
β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} |
4 | | frgrwopreg.b |
. . 3
β’ π΅ = (π β π΄) |
5 | 1, 2, 3, 4 | frgrwopreglem1 29298 |
. 2
β’ (π΄ β V β§ π΅ β V) |
6 | | hashv01gt1 14252 |
. . . 4
β’ (π΄ β V β
((β―βπ΄) = 0 β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))) |
7 | | hasheq0 14270 |
. . . . . 6
β’ (π΄ β V β
((β―βπ΄) = 0
β π΄ =
β
)) |
8 | | biidd 262 |
. . . . . 6
β’ (π΄ β V β
((β―βπ΄) = 1
β (β―βπ΄) =
1)) |
9 | | biidd 262 |
. . . . . 6
β’ (π΄ β V β (1 <
(β―βπ΄) β 1
< (β―βπ΄))) |
10 | 7, 8, 9 | 3orbi123d 1436 |
. . . . 5
β’ (π΄ β V β
(((β―βπ΄) = 0
β¨ (β―βπ΄) = 1
β¨ 1 < (β―βπ΄)) β (π΄ = β
β¨ (β―βπ΄) = 1 β¨ 1 <
(β―βπ΄)))) |
11 | | hashv01gt1 14252 |
. . . . . . 7
β’ (π΅ β V β
((β―βπ΅) = 0 β¨
(β―βπ΅) = 1 β¨
1 < (β―βπ΅))) |
12 | | hasheq0 14270 |
. . . . . . . . 9
β’ (π΅ β V β
((β―βπ΅) = 0
β π΅ =
β
)) |
13 | | biidd 262 |
. . . . . . . . 9
β’ (π΅ β V β
((β―βπ΅) = 1
β (β―βπ΅) =
1)) |
14 | | biidd 262 |
. . . . . . . . 9
β’ (π΅ β V β (1 <
(β―βπ΅) β 1
< (β―βπ΅))) |
15 | 12, 13, 14 | 3orbi123d 1436 |
. . . . . . . 8
β’ (π΅ β V β
(((β―βπ΅) = 0
β¨ (β―βπ΅) = 1
β¨ 1 < (β―βπ΅)) β (π΅ = β
β¨ (β―βπ΅) = 1 β¨ 1 <
(β―βπ΅)))) |
16 | | olc 867 |
. . . . . . . . . . 11
β’ (π΅ = β
β
((β―βπ΅) = 1 β¨
π΅ =
β
)) |
17 | 16 | olcd 873 |
. . . . . . . . . 10
β’ (π΅ = β
β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))) |
18 | 17 | 2a1d 26 |
. . . . . . . . 9
β’ (π΅ = β
β ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
19 | | orc 866 |
. . . . . . . . . . 11
β’
((β―βπ΅) =
1 β ((β―βπ΅)
= 1 β¨ π΅ =
β
)) |
20 | 19 | olcd 873 |
. . . . . . . . . 10
β’
((β―βπ΅) =
1 β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))) |
21 | 20 | 2a1d 26 |
. . . . . . . . 9
β’
((β―βπ΅) =
1 β ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
22 | | olc 867 |
. . . . . . . . . . . . 13
β’ (π΄ = β
β
((β―βπ΄) = 1 β¨
π΄ =
β
)) |
23 | 22 | orcd 872 |
. . . . . . . . . . . 12
β’ (π΄ = β
β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))) |
24 | 23 | 2a1d 26 |
. . . . . . . . . . 11
β’ (π΄ = β
β (1 <
(β―βπ΅) β
(πΊ β FriendGraph
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
25 | | orc 866 |
. . . . . . . . . . . . 13
β’
((β―βπ΄) =
1 β ((β―βπ΄)
= 1 β¨ π΄ =
β
)) |
26 | 25 | orcd 872 |
. . . . . . . . . . . 12
β’
((β―βπ΄) =
1 β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))) |
27 | 26 | 2a1d 26 |
. . . . . . . . . . 11
β’
((β―βπ΄) =
1 β (1 < (β―βπ΅) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
28 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(EdgβπΊ) =
(EdgβπΊ) |
29 | 1, 2, 3, 4, 28 | frgrwopreglem5 29307 |
. . . . . . . . . . . . . 14
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β βπ β
π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ)))) |
30 | | frgrusgr 29247 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
31 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β πΊ β USGraph) |
32 | | elrabi 3644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β {π₯ β π β£ (π·βπ₯) = πΎ} β π β π) |
33 | 32, 3 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π΄ β π β π) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π΄ β§ π₯ β π΄) β π β π) |
35 | 34 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π β π) |
36 | | rabidim1 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ β {π₯ β π β£ (π·βπ₯) = πΎ} β π₯ β π) |
37 | 36, 3 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β π΄ β π₯ β π) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π΄ β§ π₯ β π΄) β π₯ β π) |
39 | 38 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π₯ β π) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π β π₯) |
41 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π β π΄) β π β π) |
42 | 41, 4 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π΅ β π β π) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π΅ β§ π¦ β π΅) β π β π) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π β π) |
45 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β (π β π΄) β π¦ β π) |
46 | 45, 4 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β π΅ β π¦ β π) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π΅ β§ π¦ β π΅) β π¦ β π) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π¦ β π) |
49 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β π β π¦) |
50 | 1, 28 | 4cyclusnfrgr 29278 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΊ β USGraph β§ (π β π β§ π₯ β π β§ π β π₯) β§ (π β π β§ π¦ β π β§ π β π¦)) β ((({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β πΊ β FriendGraph )) |
51 | 31, 35, 39, 40, 44, 48, 49, 50 | syl133anc 1394 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β§ (π β π₯ β§ π β π¦)) β ((({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β πΊ β FriendGraph )) |
52 | 51 | exp4b 432 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β ((π β π₯ β§ π β π¦) β (({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β (({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ)) β πΊ β FriendGraph )))) |
53 | 52 | 3impd 1349 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β (((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β πΊ β FriendGraph )) |
54 | | df-nel 3051 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΊ β FriendGraph β
Β¬ πΊ β FriendGraph
) |
55 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
πΊ β FriendGraph β
(πΊ β FriendGraph
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
)))) |
56 | 54, 55 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΊ β FriendGraph β
(πΊ β FriendGraph
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
)))) |
57 | 53, 56 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β§ (π β π΅ β§ π¦ β π΅)) β (((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
58 | 57 | rexlimdvva 3206 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β USGraph β§ (π β π΄ β§ π₯ β π΄)) β (βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
59 | 58 | rexlimdvva 3206 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β USGraph β
(βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
60 | 59 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β USGraph β (πΊ β FriendGraph β
(βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
61 | 30, 60 | mpcom 38 |
. . . . . . . . . . . . . . 15
β’ (πΊ β FriendGraph β
(βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
)))) |
62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β (βπ β
π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β (EdgβπΊ) β§ {π, π₯} β (EdgβπΊ)) β§ ({π₯, π¦} β (EdgβπΊ) β§ {π¦, π} β (EdgβπΊ))) β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
)))) |
63 | 29, 62 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ΄) β§ 1
< (β―βπ΅))
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))) |
64 | 63 | 3exp 1120 |
. . . . . . . . . . . 12
β’ (πΊ β FriendGraph β (1
< (β―βπ΄)
β (1 < (β―βπ΅) β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
65 | 64 | com3l 89 |
. . . . . . . . . . 11
β’ (1 <
(β―βπ΄) β (1
< (β―βπ΅)
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
66 | 24, 27, 65 | 3jaoi 1428 |
. . . . . . . . . 10
β’ ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (1 < (β―βπ΅) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
67 | 66 | com12 32 |
. . . . . . . . 9
β’ (1 <
(β―βπ΅) β
((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
68 | 18, 21, 67 | 3jaoi 1428 |
. . . . . . . 8
β’ ((π΅ = β
β¨
(β―βπ΅) = 1 β¨
1 < (β―βπ΅))
β ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
69 | 15, 68 | syl6bi 253 |
. . . . . . 7
β’ (π΅ β V β
(((β―βπ΅) = 0
β¨ (β―βπ΅) = 1
β¨ 1 < (β―βπ΅)) β ((π΄ = β
β¨ (β―βπ΄) = 1 β¨ 1 <
(β―βπ΄)) β
(πΊ β FriendGraph
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
)))))) |
70 | 11, 69 | mpd 15 |
. . . . . 6
β’ (π΅ β V β ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (πΊ β
FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β
) β¨ ((β―βπ΅) = 1 β¨ π΅ = β
))))) |
71 | 70 | com12 32 |
. . . . 5
β’ ((π΄ = β
β¨
(β―βπ΄) = 1 β¨
1 < (β―βπ΄))
β (π΅ β V β
(πΊ β FriendGraph
β (((β―βπ΄)
= 1 β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
72 | 10, 71 | syl6bi 253 |
. . . 4
β’ (π΄ β V β
(((β―βπ΄) = 0
β¨ (β―βπ΄) = 1
β¨ 1 < (β―βπ΄)) β (π΅ β V β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
)))))) |
73 | 6, 72 | mpd 15 |
. . 3
β’ (π΄ β V β (π΅ β V β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))))) |
74 | 73 | imp 408 |
. 2
β’ ((π΄ β V β§ π΅ β V) β (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
)))) |
75 | 5, 74 | ax-mp 5 |
1
β’ (πΊ β FriendGraph β
(((β―βπ΄) = 1
β¨ π΄ = β
) β¨
((β―βπ΅) = 1 β¨
π΅ =
β
))) |