Theorem gpgprismgr4cycllem8

Description: Lemma 8 for gpgprismgr4cycl0 . (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Hypotheses	gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
	gpgprismgr4cycl.f	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
	gpgprismgr4cycl.g	No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
Assertion	gpgprismgr4cycllem8	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to F\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
2		gpgprismgr4cycl.f	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
3		gpgprismgr4cycl.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
4		df-s4	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}”⟩\mathrm{++}⟨“\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
5	2 4	eqtri	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}”⟩\mathrm{++}⟨“\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
6		gpgprismgriedgdmss	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
7		unss	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
8		prex	$$⊢\left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{V}$$
9		prex	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}\in \mathrm{V}$$
10	8 9	prss	Could not format ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
11	3	eqcomi	Could not format ( N gPetersenGr 1 ) = G : No typesetting found for |- ( N gPetersenGr 1 ) = G with typecode |-
12	11	fveq2i	Could not format ( iEdg ` ( N gPetersenGr 1 ) ) = ( iEdg ` G ) : No typesetting found for |- ( iEdg ` ( N gPetersenGr 1 ) ) = ( iEdg ` G ) with typecode |-
13	12	dmeqi	Could not format dom ( iEdg ` ( N gPetersenGr 1 ) ) = dom ( iEdg ` G ) : No typesetting found for |- dom ( iEdg ` ( N gPetersenGr 1 ) ) = dom ( iEdg ` G ) with typecode |-
14	13	eleq2i	Could not format ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
15	14	birani	Could not format ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
16	10 15	sylbir	Could not format ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
17	16	adantr	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
18	7 17	sylbir	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
19	6 18	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
20		prex	$$⊢\left\{⟨1,1⟩,⟨0,1⟩\right\}\in \mathrm{V}$$
21		prex	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}$$
22	20 21	prss	Could not format ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
23		prcom	$$⊢\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
24	23 13	eleq12i	Could not format ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
25	24	birani	Could not format ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
26	22 25	sylbir	Could not format ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
27	26	adantl	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
28	7 27	sylbir	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) ) with typecode |-
29	6 28	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
30	13	eleq2i	Could not format ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
31	30	bilani	Could not format ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
32	22 31	sylbir	Could not format ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
33	32	adantl	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
34	7 33	sylbir	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
35	6 34	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
36	19 29 35	s3cld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}”⟩\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(G\right)$$
37		simpr	Could not format ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
38	10 37	sylbir	Could not format ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
39		prcom	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
40	3	fveq2i	Could not format ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) : No typesetting found for |- ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) with typecode |-
41	40	dmeqi	Could not format dom ( iEdg ` G ) = dom ( iEdg ` ( N gPetersenGr 1 ) ) : No typesetting found for |- dom ( iEdg ` G ) = dom ( iEdg ` ( N gPetersenGr 1 ) ) with typecode |-
42	38 39 41	3eltr4g	Could not format ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
43	42	adantr	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
44	7 43	sylbir	Could not format ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) : No typesetting found for |- ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) ) with typecode |-
45	6 44	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
46	5 36 45	cats1cld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to F\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(G\right)$$