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	biimpi	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 |-
16	15	adantr	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 |-
17	10 16	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 |-
18	17	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 |-
19	7 18	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 |-
20	6 19	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
21		prex	$$⊢\left\{⟨1,1⟩,⟨0,1⟩\right\}\in \mathrm{V}$$
22		prex	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}$$
23	21 22	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 |-
24		prcom	$$⊢\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
25	24 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 |-
26	25	biimpi	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 |-
27	26	adantr	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 |-
28	23 27	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 |-
29	28	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 |-
30	7 29	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 |-
31	6 30	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
32	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 |-
33	32	biimpi	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 |-
34	33	adantl	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 |-
35	23 34	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 |-
36	35	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 |-
37	7 36	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 |-
38	6 37	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
39	20 31 38	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)$$
40		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 |-
41	10 40	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 |-
42		prcom	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
43	3	fveq2i	Could not format ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) : No typesetting found for |- ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) with typecode |-
44	43	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 |-
45	41 42 44	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 |-
46	45	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 |-
47	7 46	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 |-
48	6 47	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{dom}\mathrm{iEdg}\left(G\right)$$
49	5 39 48	cats1cld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to F\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left(G\right)$$