Step | Hyp | Ref
| Expression |
1 | | frgrreggt1.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | | eqid 2736 |
. . . 4
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | frgrregorufrg 29270 |
. . 3
β’ (πΊ β FriendGraph β
βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
4 | 3 | 3ad2ant1 1133 |
. 2
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
5 | 1 | frgrogt3nreg 29341 |
. 2
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
βπ β
β0 Β¬ πΊ
RegUSGraph π) |
6 | | frgrusgr 29205 |
. . . . . . 7
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
7 | 6 | anim1i 615 |
. . . . . 6
β’ ((πΊ β FriendGraph β§ π β Fin) β (πΊ β USGraph β§ π β Fin)) |
8 | 1 | isfusgr 28266 |
. . . . . 6
β’ (πΊ β FinUSGraph β (πΊ β USGraph β§ π β Fin)) |
9 | 7, 8 | sylibr 233 |
. . . . 5
β’ ((πΊ β FriendGraph β§ π β Fin) β πΊ β
FinUSGraph) |
10 | 9 | 3adant3 1132 |
. . . 4
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
πΊ β
FinUSGraph) |
11 | | 0red 11158 |
. . . . . . . 8
β’ ((π β Fin β§ 3 <
(β―βπ)) β 0
β β) |
12 | | 3re 12233 |
. . . . . . . . 9
β’ 3 β
β |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ ((π β Fin β§ 3 <
(β―βπ)) β 3
β β) |
14 | | hashcl 14256 |
. . . . . . . . . 10
β’ (π β Fin β
(β―βπ) β
β0) |
15 | 14 | nn0red 12474 |
. . . . . . . . 9
β’ (π β Fin β
(β―βπ) β
β) |
16 | 15 | adantr 481 |
. . . . . . . 8
β’ ((π β Fin β§ 3 <
(β―βπ)) β
(β―βπ) β
β) |
17 | | 3pos 12258 |
. . . . . . . . 9
β’ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ ((π β Fin β§ 3 <
(β―βπ)) β 0
< 3) |
19 | | simpr 485 |
. . . . . . . 8
β’ ((π β Fin β§ 3 <
(β―βπ)) β 3
< (β―βπ)) |
20 | 11, 13, 16, 18, 19 | lttrd 11316 |
. . . . . . 7
β’ ((π β Fin β§ 3 <
(β―βπ)) β 0
< (β―βπ)) |
21 | 20 | gt0ne0d 11719 |
. . . . . 6
β’ ((π β Fin β§ 3 <
(β―βπ)) β
(β―βπ) β
0) |
22 | | hasheq0 14263 |
. . . . . . . 8
β’ (π β Fin β
((β―βπ) = 0
β π =
β
)) |
23 | 22 | adantr 481 |
. . . . . . 7
β’ ((π β Fin β§ 3 <
(β―βπ)) β
((β―βπ) = 0
β π =
β
)) |
24 | 23 | necon3bid 2988 |
. . . . . 6
β’ ((π β Fin β§ 3 <
(β―βπ)) β
((β―βπ) β 0
β π β
β
)) |
25 | 21, 24 | mpbid 231 |
. . . . 5
β’ ((π β Fin β§ 3 <
(β―βπ)) β
π β
β
) |
26 | 25 | 3adant1 1130 |
. . . 4
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
π β
β
) |
27 | 1 | fusgrn0degnn0 28447 |
. . . 4
β’ ((πΊ β FinUSGraph β§ π β β
) β
βπ‘ β π βπ β β0
((VtxDegβπΊ)βπ‘) = π) |
28 | 10, 26, 27 | syl2anc 584 |
. . 3
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
βπ‘ β π βπ β β0
((VtxDegβπΊ)βπ‘) = π) |
29 | | r19.26 3114 |
. . . . . . . 8
β’
(βπ β
β0 ((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β (βπ β β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ βπ β β0 Β¬ πΊ RegUSGraph π)) |
30 | | simpllr 774 |
. . . . . . . . . 10
β’ ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
π β
β0) |
31 | | fveqeq2 6851 |
. . . . . . . . . . . . . . 15
β’ (π’ = π‘ β (((VtxDegβπΊ)βπ’) = π β ((VtxDegβπΊ)βπ‘) = π)) |
32 | 31 | rspcev 3581 |
. . . . . . . . . . . . . 14
β’ ((π‘ β π β§ ((VtxDegβπΊ)βπ‘) = π) β βπ’ β π ((VtxDegβπΊ)βπ’) = π) |
33 | 32 | ad4ant13 749 |
. . . . . . . . . . . . 13
β’ ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
βπ’ β π ((VtxDegβπΊ)βπ’) = π) |
34 | | ornld 1060 |
. . . . . . . . . . . . 13
β’
(βπ’ β
π ((VtxDegβπΊ)βπ’) = π β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
(((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
36 | 35 | adantr 481 |
. . . . . . . . . . 11
β’
(((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β§
π = π) β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
37 | | eqeq2 2748 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((VtxDegβπΊ)βπ’) = π β ((VtxDegβπΊ)βπ’) = π)) |
38 | 37 | rexbidv 3175 |
. . . . . . . . . . . . . . 15
β’ (π = π β (βπ’ β π ((VtxDegβπΊ)βπ’) = π β βπ’ β π ((VtxDegβπΊ)βπ’) = π)) |
39 | | breq2 5109 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΊ RegUSGraph π β πΊ RegUSGraph π)) |
40 | 39 | orbi1d 915 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)) β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
41 | 38, 40 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π = π β ((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))))) |
42 | 39 | notbid 317 |
. . . . . . . . . . . . . 14
β’ (π = π β (Β¬ πΊ RegUSGraph π β Β¬ πΊ RegUSGraph π)) |
43 | 41, 42 | anbi12d 631 |
. . . . . . . . . . . . 13
β’ (π = π β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β ((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π))) |
44 | 43 | imbi1d 341 |
. . . . . . . . . . . 12
β’ (π = π β ((((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)) β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
45 | 44 | adantl 482 |
. . . . . . . . . . 11
β’
(((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β§
π = π) β ((((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)) β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
46 | 36, 45 | mpbird 256 |
. . . . . . . . . 10
β’
(((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β§
π = π) β (((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
47 | 30, 46 | rspcimdv 3571 |
. . . . . . . . 9
β’ ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
(βπ β
β0 ((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
48 | 47 | com12 32 |
. . . . . . . 8
β’
(βπ β
β0 ((βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ Β¬ πΊ RegUSGraph π) β ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
49 | 29, 48 | sylbir 234 |
. . . . . . 7
β’
((βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β§ βπ β β0 Β¬ πΊ RegUSGraph π) β ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) |
50 | 49 | expcom 414 |
. . . . . 6
β’
(βπ β
β0 Β¬ πΊ
RegUSGraph π β
(βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
51 | 50 | com13 88 |
. . . . 5
β’ ((((π‘ β π β§ π β β0) β§
((VtxDegβπΊ)βπ‘) = π) β§ (πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ))) β
(βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β (βπ β β0 Β¬ πΊ RegUSGraph π β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
52 | 51 | exp31 420 |
. . . 4
β’ ((π‘ β π β§ π β β0) β
(((VtxDegβπΊ)βπ‘) = π β ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
(βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β (βπ β β0 Β¬ πΊ RegUSGraph π β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))))) |
53 | 52 | rexlimivv 3196 |
. . 3
β’
(βπ‘ β
π βπ β β0
((VtxDegβπΊ)βπ‘) = π β ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
(βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β (βπ β β0 Β¬ πΊ RegUSGraph π β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))))) |
54 | 28, 53 | mpcom 38 |
. 2
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
(βπ β
β0 (βπ’ β π ((VtxDegβπΊ)βπ’) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ))) β (βπ β β0 Β¬ πΊ RegUSGraph π β βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)))) |
55 | 4, 5, 54 | mp2d 49 |
1
β’ ((πΊ β FriendGraph β§ π β Fin β§ 3 <
(β―βπ)) β
βπ£ β π βπ€ β (π β {π£}){π£, π€} β (EdgβπΊ)) |