Step | Hyp | Ref
| Expression |
1 | | neirr 2803 |
. . . . . . . . . . . . . . . . . 18
|
2 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
Edg Edg |
3 | 2 | usgredgne 26098 |
. . . . . . . . . . . . . . . . . . 19
USGraph
Edg |
4 | 3 | ex 450 |
. . . . . . . . . . . . . . . . . 18
USGraph Edg |
5 | 1, 4 | mtoi 190 |
. . . . . . . . . . . . . . . . 17
USGraph
Edg |
6 | 5 | adantl 482 |
. . . . . . . . . . . . . . . 16
USGraph
Edg |
7 | 6 | intnanrd 963 |
. . . . . . . . . . . . . . 15
USGraph
Edg
Edg |
8 | | prex 4909 |
. . . . . . . . . . . . . . . 16
|
9 | | prex 4909 |
. . . . . . . . . . . . . . . 16
|
10 | 8, 9 | prss 4351 |
. . . . . . . . . . . . . . 15
Edg
Edg
Edg |
11 | 7, 10 | sylnib 318 |
. . . . . . . . . . . . . 14
USGraph
Edg |
12 | | neirr 2803 |
. . . . . . . . . . . . . . . . . 18
|
13 | 2 | usgredgne 26098 |
. . . . . . . . . . . . . . . . . . 19
USGraph
Edg |
14 | 13 | ex 450 |
. . . . . . . . . . . . . . . . . 18
USGraph Edg |
15 | 12, 14 | mtoi 190 |
. . . . . . . . . . . . . . . . 17
USGraph
Edg |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . 16
USGraph
Edg |
17 | 16 | intnand 962 |
. . . . . . . . . . . . . . 15
USGraph
Edg
Edg |
18 | | prex 4909 |
. . . . . . . . . . . . . . . 16
|
19 | | prex 4909 |
. . . . . . . . . . . . . . . 16
|
20 | 18, 19 | prss 4351 |
. . . . . . . . . . . . . . 15
Edg
Edg
Edg |
21 | 17, 20 | sylnib 318 |
. . . . . . . . . . . . . 14
USGraph
Edg |
22 | | ioran 511 |
. . . . . . . . . . . . . 14
Edg
Edg
Edg Edg |
23 | 11, 21, 22 | sylanbrc 698 |
. . . . . . . . . . . . 13
USGraph
Edg
Edg |
24 | | preq1 4268 |
. . . . . . . . . . . . . . . . . 18
|
25 | | preq1 4268 |
. . . . . . . . . . . . . . . . . 18
|
26 | 24, 25 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
|
27 | 26 | sseq1d 3632 |
. . . . . . . . . . . . . . . 16
Edg
Edg |
28 | | preq1 4268 |
. . . . . . . . . . . . . . . . . 18
|
29 | | preq1 4268 |
. . . . . . . . . . . . . . . . . 18
|
30 | 28, 29 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | sseq1d 3632 |
. . . . . . . . . . . . . . . 16
Edg
Edg |
32 | 27, 31 | rexprg 4235 |
. . . . . . . . . . . . . . 15
Edg
Edg
Edg |
33 | 32 | 3adant3 1081 |
. . . . . . . . . . . . . 14
Edg
Edg
Edg |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
USGraph Edg
Edg
Edg |
35 | 23, 34 | mtbird 315 |
. . . . . . . . . . . 12
USGraph
Edg |
36 | | reurex 3160 |
. . . . . . . . . . . 12
Edg Edg |
37 | 35, 36 | nsyl 135 |
. . . . . . . . . . 11
USGraph
Edg |
38 | 37 | orcd 407 |
. . . . . . . . . 10
USGraph
Edg
Edg |
39 | | rexnal 2995 |
. . . . . . . . . . . . . 14
Edg
Edg |
40 | 39 | bicomi 214 |
. . . . . . . . . . . . 13
Edg
Edg |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
42 | | difprsn1 4330 |
. . . . . . . . . . . . . . 15
|
43 | 42 | 3ad2ant3 1084 |
. . . . . . . . . . . . . 14
|
44 | 43 | adantr 481 |
. . . . . . . . . . . . 13
USGraph |
45 | 44 | rexeqdv 3145 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
46 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | preq2d 4275 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
Edg
Edg |
49 | 48 | reubidv 3126 |
. . . . . . . . . . . . . . . 16
Edg
Edg |
50 | 49 | notbid 308 |
. . . . . . . . . . . . . . 15
Edg
Edg |
51 | 50 | rexsng 4219 |
. . . . . . . . . . . . . 14
Edg
Edg |
52 | 51 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
Edg
Edg |
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
54 | 41, 45, 53 | 3bitrd 294 |
. . . . . . . . . . 11
USGraph
Edg
Edg |
55 | | rexnal 2995 |
. . . . . . . . . . . . . 14
Edg
Edg |
56 | 55 | bicomi 214 |
. . . . . . . . . . . . 13
Edg
Edg |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
58 | | difprsn2 4331 |
. . . . . . . . . . . . . . 15
|
59 | 58 | 3ad2ant3 1084 |
. . . . . . . . . . . . . 14
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . 13
USGraph |
61 | 60 | rexeqdv 3145 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
62 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | preq2d 4275 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
Edg
Edg |
65 | 64 | reubidv 3126 |
. . . . . . . . . . . . . . . 16
Edg
Edg |
66 | 65 | notbid 308 |
. . . . . . . . . . . . . . 15
Edg
Edg |
67 | 66 | rexsng 4219 |
. . . . . . . . . . . . . 14
Edg
Edg |
68 | 67 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Edg
Edg |
69 | 68 | adantr 481 |
. . . . . . . . . . . 12
USGraph
Edg
Edg |
70 | 57, 61, 69 | 3bitrd 294 |
. . . . . . . . . . 11
USGraph
Edg
Edg |
71 | 54, 70 | orbi12d 746 |
. . . . . . . . . 10
USGraph
Edg
Edg
Edg
Edg |
72 | 38, 71 | mpbird 247 |
. . . . . . . . 9
USGraph
Edg
Edg |
73 | | sneq 4187 |
. . . . . . . . . . . . . . 15
|
74 | 73 | difeq2d 3728 |
. . . . . . . . . . . . . 14
|
75 | | preq2 4269 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | preq1d 4274 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
Edg
Edg |
78 | 77 | reubidv 3126 |
. . . . . . . . . . . . . 14
Edg
Edg |
79 | 74, 78 | raleqbidv 3152 |
. . . . . . . . . . . . 13
Edg
Edg |
80 | 79 | notbid 308 |
. . . . . . . . . . . 12
Edg
Edg |
81 | | sneq 4187 |
. . . . . . . . . . . . . . 15
|
82 | 81 | difeq2d 3728 |
. . . . . . . . . . . . . 14
|
83 | | preq2 4269 |
. . . . . . . . . . . . . . . . 17
|
84 | 83 | preq1d 4274 |
. . . . . . . . . . . . . . . 16
|
85 | 84 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
Edg
Edg |
86 | 85 | reubidv 3126 |
. . . . . . . . . . . . . 14
Edg
Edg |
87 | 82, 86 | raleqbidv 3152 |
. . . . . . . . . . . . 13
Edg
Edg |
88 | 87 | notbid 308 |
. . . . . . . . . . . 12
Edg
Edg |
89 | 80, 88 | rexprg 4235 |
. . . . . . . . . . 11
Edg
Edg
Edg |
90 | 89 | 3adant3 1081 |
. . . . . . . . . 10
Edg
Edg
Edg |
91 | 90 | adantr 481 |
. . . . . . . . 9
USGraph
Edg
Edg
Edg |
92 | 72, 91 | mpbird 247 |
. . . . . . . 8
USGraph
Edg |
93 | | rexnal 2995 |
. . . . . . . 8
Edg
Edg |
94 | 92, 93 | sylib 208 |
. . . . . . 7
USGraph
Edg |
95 | 94 | intnand 962 |
. . . . . 6
USGraph
USGraph
Edg |
96 | 95 | adantlr 751 |
. . . . 5
Vtx
USGraph
USGraph
Edg |
97 | | id 22 |
. . . . . . . . . 10
Vtx Vtx |
98 | | difeq1 3721 |
. . . . . . . . . . 11
Vtx Vtx
|
99 | | reueq1 3140 |
. . . . . . . . . . 11
Vtx Vtx Edg Edg |
100 | 98, 99 | raleqbidv 3152 |
. . . . . . . . . 10
Vtx Vtx
Vtx Edg
Edg |
101 | 97, 100 | raleqbidv 3152 |
. . . . . . . . 9
Vtx Vtx
Vtx Vtx Edg
Edg |
102 | 101 | anbi2d 740 |
. . . . . . . 8
Vtx USGraph Vtx
Vtx Vtx Edg USGraph
Edg |
103 | 102 | notbid 308 |
. . . . . . 7
Vtx
USGraph Vtx
Vtx Vtx Edg
USGraph
Edg |
104 | 103 | adantl 482 |
. . . . . 6
Vtx USGraph Vtx
Vtx Vtx Edg
USGraph
Edg |
105 | 104 | adantr 481 |
. . . . 5
Vtx
USGraph
USGraph Vtx
Vtx Vtx Edg
USGraph
Edg |
106 | 96, 105 | mpbird 247 |
. . . 4
Vtx
USGraph
USGraph Vtx
Vtx Vtx Edg |
107 | | df-nel 2898 |
. . . . 5
FriendGraph FriendGraph |
108 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
109 | 108, 2 | frgrusgrfrcond 27123 |
. . . . 5
FriendGraph USGraph
Vtx Vtx
Vtx Edg |
110 | 107, 109 | xchbinx 324 |
. . . 4
FriendGraph USGraph Vtx
Vtx Vtx Edg |
111 | 106, 110 | sylibr 224 |
. . 3
Vtx
USGraph FriendGraph |
112 | 111 | expcom 451 |
. 2
USGraph
Vtx FriendGraph |
113 | | frgrusgr 27124 |
. . . . 5
FriendGraph USGraph |
114 | 113 | con3i 150 |
. . . 4
USGraph
FriendGraph |
115 | 114, 107 | sylibr 224 |
. . 3
USGraph
FriendGraph |
116 | 115 | a1d 25 |
. 2
USGraph
Vtx FriendGraph |
117 | 112, 116 | pm2.61i 176 |
1
Vtx FriendGraph |