Step |
Hyp |
Ref |
Expression |
1 |
|
konigsberg.v |
β’ π = ( 0 ... 3 ) |
2 |
|
konigsberg.e |
β’ πΈ = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© |
3 |
|
konigsberg.g |
β’ πΊ = β¨ π , πΈ β© |
4 |
1 2
|
opeq12i |
β’ β¨ π , πΈ β© = β¨ ( 0 ... 3 ) , β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β© |
5 |
3 4
|
eqtri |
β’ πΊ = β¨ ( 0 ... 3 ) , β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β© |
6 |
5
|
fveq2i |
β’ ( iEdg β πΊ ) = ( iEdg β β¨ ( 0 ... 3 ) , β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β© ) |
7 |
|
ovex |
β’ ( 0 ... 3 ) β V |
8 |
|
s7cli |
β’ β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β Word V |
9 |
|
opiedgfv |
β’ ( ( ( 0 ... 3 ) β V β§ β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β Word V ) β ( iEdg β β¨ ( 0 ... 3 ) , β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β© ) = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© ) |
10 |
7 8 9
|
mp2an |
β’ ( iEdg β β¨ ( 0 ... 3 ) , β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© β© ) = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© |
11 |
6 10
|
eqtri |
β’ ( iEdg β πΊ ) = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© |