Theorem grlimedgnedg

Description: In general, the image of an edge of a graph by a local isomprphism is not an edge of the other graph, proven by an example (see gpg5edgnedg ). This theorem proves that the analogon ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F e. ( G GraphLocIso H ) /\ K e. I ) ) -> ( F " K ) e. E ) of grimedgi for ordinarily isomorphic graphs does not hold in general. (Contributed by AV, 30-Dec-2025)

	Ref	Expression
Assertion	grlimedgnedg	$$⊢\exists g\in \mathrm{USGraph}\exists h\in \mathrm{USGraph}\exists f\in \left(g\mathrm{GraphLocIso}h\right)\exists a\in \mathrm{Vtx}\left(g\right)\exists b\in \mathrm{Vtx}\left(g\right)\left(\left\{a,b\right\}\in \mathrm{Edg}\left(g\right)\wedge \left\{f\left(a\right),f\left(b\right)\right\}\notin \mathrm{Edg}\left(h\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( g GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso h ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( g GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso h ) ) with typecode |-
2		fveq2	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( Vtx ` g ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( Vtx ` g ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) ) with typecode |-
3		fveq2	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( Edg ` g ) = ( Edg ` ( 5 gPetersenGr 1 ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( Edg ` g ) = ( Edg ` ( 5 gPetersenGr 1 ) ) ) with typecode |-
4	3	eleq2d	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( { a , b } e. ( Edg ` g ) <-> { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( { a , b } e. ( Edg ` g ) <-> { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) with typecode |-
5	4	anbi1d	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) with typecode |-
6	2 5	rexeqbidv	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) with typecode |-
7	2 6	rexeqbidv	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) with typecode |-
8	1 7	rexeqbidv	Could not format ( g = ( 5 gPetersenGr 1 ) -> ( E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) : No typesetting found for |- ( g = ( 5 gPetersenGr 1 ) -> ( E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) ) with typecode |-
9		oveq2	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( ( 5 gPetersenGr 1 ) GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( ( 5 gPetersenGr 1 ) GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) with typecode |-
10		eqidd	Could not format ( h = ( 5 gPetersenGr 2 ) -> { ( f ` a ) , ( f ` b ) } = { ( f ` a ) , ( f ` b ) } ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> { ( f ` a ) , ( f ` b ) } = { ( f ` a ) , ( f ` b ) } ) with typecode |-
11		fveq2	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( Edg ` h ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( Edg ` h ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
12	10 11	neleq12d	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) <-> { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) <-> { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
13	12	anbi2d	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
14	13	2rexbidv	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
15	9 14	rexeqbidv	Could not format ( h = ( 5 gPetersenGr 2 ) -> ( E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( h = ( 5 gPetersenGr 2 ) -> ( E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
16		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
17		gpgprismgrusgra	Could not format ( 5 e. ( ZZ>= ` 3 ) -> ( 5 gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( 5 e. ( ZZ>= ` 3 ) -> ( 5 gPetersenGr 1 ) e. USGraph ) with typecode |-
18	16 17	mp1i	Could not format ( T. -> ( 5 gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( T. -> ( 5 gPetersenGr 1 ) e. USGraph ) with typecode |-
19		pgjsgr	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-
20	19	a1i	Could not format ( T. -> ( 5 gPetersenGr 2 ) e. USGraph ) : No typesetting found for |- ( T. -> ( 5 gPetersenGr 2 ) e. USGraph ) with typecode |-
21		fveq1	$$⊢f={\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\to f\left(a\right)=\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(a\right)$$
22		fveq1	$$⊢f={\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\to f\left(b\right)=\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)$$
23	21 22	preq12d	$$⊢f={\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\to \left\{f\left(a\right),f\left(b\right)\right\}=\left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(a\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)\right\}$$
24		eqidd	Could not format ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
25	23 24	neleq12d	Could not format ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
26	25	anbi2d	Could not format ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
27		preq1	$$⊢a=⟨1,0⟩\to \left\{a,b\right\}=\left\{⟨1,0⟩,b\right\}$$
28	27	eleq1d	Could not format ( a = <. 1 , 0 >. -> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) : No typesetting found for |- ( a = <. 1 , 0 >. -> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) with typecode |-
29		fveq2	$$⊢a=⟨1,0⟩\to \left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(a\right)=\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right)$$
30	29	preq1d	$$⊢a=⟨1,0⟩\to \left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(a\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)\right\}=\left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)\right\}$$
31		eqidd	Could not format ( a = <. 1 , 0 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( a = <. 1 , 0 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
32	30 31	neleq12d	Could not format ( a = <. 1 , 0 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( a = <. 1 , 0 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
33	28 32	anbi12d	Could not format ( a = <. 1 , 0 >. -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( a = <. 1 , 0 >. -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
34		preq2	$$⊢b=⟨1,1⟩\to \left\{⟨1,0⟩,b\right\}=\left\{⟨1,0⟩,⟨1,1⟩\right\}$$
35	34	eleq1d	Could not format ( b = <. 1 , 1 >. -> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) : No typesetting found for |- ( b = <. 1 , 1 >. -> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) ) with typecode |-
36		fveq2	$$⊢b=⟨1,1⟩\to \left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)=\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,1⟩\right)$$
37	36	preq2d	$$⊢b=⟨1,1⟩\to \left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(b\right)\right\}=\left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,1⟩\right)\right\}$$
38		eqidd	Could not format ( b = <. 1 , 1 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( b = <. 1 , 1 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
39	37 38	neleq12d	Could not format ( b = <. 1 , 1 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( b = <. 1 , 1 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
40	35 39	anbi12d	Could not format ( b = <. 1 , 1 >. -> ( ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) : No typesetting found for |- ( b = <. 1 , 1 >. -> ( ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) ) with typecode |-
41		gpg5grlim	Could not format ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) with typecode |-
42	41	a1i	Could not format ( T. -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( T. -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) with typecode |-
43		1ex	$$⊢1\in \mathrm{V}$$
44	43	prid2	$$⊢1\in \left\{0,1\right\}$$
45		5nn	$$⊢5\in \mathbb{N}$$
46		lbfzo0	$$⊢0\in \left(0..^5\right)\leftrightarrow 5\in \mathbb{N}$$
47	45 46	mpbir	$$⊢0\in \left(0..^5\right)$$
48	44 47	opelxpii	$$⊢⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^5\right)\right)$$
49		1elfzo1ceilhalf1	$$⊢5\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
50	16 49	ax-mp	$$⊢1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
51		eqid	$$⊢\left(1..^⌈\frac{5}{2}⌉\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
52		eqid	$$⊢\left(0..^5\right)=\left(0..^5\right)$$
53	51 52	gpgvtx	Could not format ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : No typesetting found for |- ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) with typecode |-
54	45 50 53	mp2an	Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) with typecode |-
55	48 54	eleqtrri	Could not format <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) : No typesetting found for |- <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) with typecode |-
56	55	a1i	Could not format ( T. -> <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) : No typesetting found for |- ( T. -> <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) with typecode |-
57		1nn0	$$⊢1\in {\mathbb{N}}_0$$
58	45	nnzi	$$⊢5\in \mathbb{Z}$$
59		1lt5	$$⊢1<5$$
60		elfzo0z	$$⊢1\in \left(0..^5\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge 5\in \mathbb{Z}\wedge 1<5\right)$$
61	57 58 59 60	mpbir3an	$$⊢1\in \left(0..^5\right)$$
62	44 61	opelxpii	$$⊢⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^5\right)\right)$$
63	62 54	eleqtrri	Could not format <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) : No typesetting found for |- <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) with typecode |-
64	63	a1i	Could not format ( T. -> <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) : No typesetting found for |- ( T. -> <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) with typecode |-
65		gpg5edgnedg	Could not format ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
66		fvresi	$$⊢⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^5\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right)=⟨1,0⟩$$
67	48 66	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right)=⟨1,0⟩$$
68		fvresi	$$⊢⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^5\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,1⟩\right)=⟨1,1⟩$$
69	62 68	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,1⟩\right)=⟨1,1⟩$$
70	67 69	preq12i	$$⊢\left\{\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,0⟩\right),\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right)\left(⟨1,1⟩\right)\right\}=\left\{⟨1,0⟩,⟨1,1⟩\right\}$$
71		neleq1	Could not format ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } = { <. 1 , 0 >. , <. 1 , 1 >. } -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } = { <. 1 , 0 >. , <. 1 , 1 >. } -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
72	70 71	ax-mp	Could not format ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
73	72	anbi2i	Could not format ( ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
74	65 73	mpbir	Could not format ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
75	74	a1i	Could not format ( T. -> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( T. -> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
76	26 33 40 42 56 64 75	3rspcedvdw	Could not format ( T. -> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( T. -> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
77	8 15 18 20 76	2rspcedvdw	$$⊢\top \to \exists g\in \mathrm{USGraph}\exists h\in \mathrm{USGraph}\exists f\in \left(g\mathrm{GraphLocIso}h\right)\exists a\in \mathrm{Vtx}\left(g\right)\exists b\in \mathrm{Vtx}\left(g\right)\left(\left\{a,b\right\}\in \mathrm{Edg}\left(g\right)\wedge \left\{f\left(a\right),f\left(b\right)\right\}\notin \mathrm{Edg}\left(h\right)\right)$$
78	77	mptru	$$⊢\exists g\in \mathrm{USGraph}\exists h\in \mathrm{USGraph}\exists f\in \left(g\mathrm{GraphLocIso}h\right)\exists a\in \mathrm{Vtx}\left(g\right)\exists b\in \mathrm{Vtx}\left(g\right)\left(\left\{a,b\right\}\in \mathrm{Edg}\left(g\right)\wedge \left\{f\left(a\right),f\left(b\right)\right\}\notin \mathrm{Edg}\left(h\right)\right)$$