Step | Hyp | Ref
| Expression |
1 | | df-frgr 27121 |
. . 3
FriendGraph USGraph Vtx Edg
|
2 | 1 | eleq2i 2693 |
. 2
FriendGraph USGraph Vtx Edg
|
3 | | eleq1 2689 |
. . . 4
USGraph
USGraph |
4 | | fveq2 6191 |
. . . . . 6
Vtx Vtx |
5 | | isfrgr.v |
. . . . . 6
Vtx |
6 | 4, 5 | syl6eqr 2674 |
. . . . 5
Vtx |
7 | 6 | difeq1d 3727 |
. . . . . 6
Vtx |
8 | | reueq1 3140 |
. . . . . . . 8
Vtx
Vtx Edg
Edg |
9 | 6, 8 | syl 17 |
. . . . . . 7
Vtx Edg
Edg |
10 | | fveq2 6191 |
. . . . . . . . . 10
Edg Edg |
11 | | isfrgr.e |
. . . . . . . . . 10
Edg |
12 | 10, 11 | syl6eqr 2674 |
. . . . . . . . 9
Edg |
13 | 12 | sseq2d 3633 |
. . . . . . . 8
Edg |
14 | 13 | reubidv 3126 |
. . . . . . 7
Edg |
15 | 9, 14 | bitrd 268 |
. . . . . 6
Vtx Edg
|
16 | 7, 15 | raleqbidv 3152 |
. . . . 5
Vtx Vtx Edg |
17 | 6, 16 | raleqbidv 3152 |
. . . 4
Vtx Vtx
Vtx Edg
|
18 | 3, 17 | anbi12d 747 |
. . 3
USGraph
Vtx Vtx
Vtx Edg USGraph
|
19 | | eleq1 2689 |
. . . . 5
USGraph
USGraph |
20 | | fvexd 6203 |
. . . . . 6
Vtx |
21 | | fveq2 6191 |
. . . . . 6
Vtx Vtx |
22 | | fvexd 6203 |
. . . . . . 7
Vtx Edg |
23 | | fveq2 6191 |
. . . . . . . 8
Edg Edg |
24 | 23 | adantr 481 |
. . . . . . 7
Vtx Edg Edg |
25 | | simpr 477 |
. . . . . . . . 9
Vtx Vtx |
26 | 25 | adantr 481 |
. . . . . . . 8
Vtx Edg Vtx |
27 | | difeq1 3721 |
. . . . . . . . . 10
Vtx
Vtx |
28 | 27 | ad2antlr 763 |
. . . . . . . . 9
Vtx Edg Vtx |
29 | | reueq1 3140 |
. . . . . . . . . . 11
Vtx
Vtx |
30 | 29 | ad2antlr 763 |
. . . . . . . . . 10
Vtx Edg
Vtx |
31 | | simpr 477 |
. . . . . . . . . . . 12
Vtx Edg Edg |
32 | 31 | sseq2d 3633 |
. . . . . . . . . . 11
Vtx Edg
Edg |
33 | 32 | reubidv 3126 |
. . . . . . . . . 10
Vtx Edg Vtx Vtx Edg |
34 | 30, 33 | bitrd 268 |
. . . . . . . . 9
Vtx Edg
Vtx Edg |
35 | 28, 34 | raleqbidv 3152 |
. . . . . . . 8
Vtx Edg Vtx Vtx Edg |
36 | 26, 35 | raleqbidv 3152 |
. . . . . . 7
Vtx Edg
Vtx
Vtx Vtx Edg |
37 | 22, 24, 36 | sbcied2 3473 |
. . . . . 6
Vtx Edg
Vtx
Vtx Vtx Edg |
38 | 20, 21, 37 | sbcied2 3473 |
. . . . 5
Vtx Edg
Vtx Vtx
Vtx Edg |
39 | 19, 38 | anbi12d 747 |
. . . 4
USGraph Vtx Edg
USGraph Vtx
Vtx Vtx Edg |
40 | 39 | cbvabv 2747 |
. . 3
USGraph Vtx Edg
USGraph Vtx
Vtx Vtx Edg |
41 | 18, 40 | elab2g 3353 |
. 2
USGraph Vtx Edg
USGraph
|
42 | 2, 41 | syl5bb 272 |
1
FriendGraph USGraph
|