gpgprismgriedgdmss

Description: A subset of the index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025)

		Ref	Expression
	Assertion	gpgprismgriedgdmss	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 𝑁 ∈ ℕ )
2		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
3	1 2	sylibr	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 0 ∈ ( 0 ..^ 𝑁 ) )
4		opeq2	⊢ ( 𝑥 = 0 → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , 0 ⟩ )
5		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 + 1 ) = ( 0 + 1 ) )
6		0p1e1	⊢ ( 0 + 1 ) = 1
7	5 6	eqtrdi	⊢ ( 𝑥 = 0 → ( 𝑥 + 1 ) = 1 )
8	7	oveq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 + 1 ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
9	8	opeq2d	⊢ ( 𝑥 = 0 → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 1 mod 𝑁 ) ⟩ )
10	4 9	preq12d	⊢ ( 𝑥 = 0 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( 1 mod 𝑁 ) ⟩ } )
11	10	eqeq2d	⊢ ( 𝑥 = 0 → ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( 1 mod 𝑁 ) ⟩ } ) )
12	11	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝑥 = 0 ) → ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( 1 mod 𝑁 ) ⟩ } ) )
13		uzuzle23	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 𝑁 ∈ ( ℤ_≥ ‘ 2 ) )
14		eluz2b1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
15		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
16	15	anim1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
17	14 16	sylbi	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
18		1mod	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )
19	13 17 18	3syl	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( 1 mod 𝑁 ) = 1 )
20	19	eqcomd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 1 = ( 1 mod 𝑁 ) )
21	20	opeq2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ⟨ 0 , 1 ⟩ = ⟨ 0 , ( 1 mod 𝑁 ) ⟩ )
22	21	preq2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( 1 mod 𝑁 ) ⟩ } )
23	3 12 22	rspcedvd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } )
24	23	3mix1d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
25		3r19.43	⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
26	24 25	sylibr	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
27		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
28		eqid	⊢ ( 𝑁 gPetersenGr 1 ) = ( 𝑁 gPetersenGr 1 )
29	27 28	gpgprismgriedgdmel	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )
30	26 29	mpbird	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
31		opeq2	⊢ ( 𝑥 = 0 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 0 ⟩ )
32	4 31	preq12d	⊢ ( 𝑥 = 0 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
33	32	eqeq2d	⊢ ( 𝑥 = 0 → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ) )
34	33	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝑥 = 0 ) → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ) )
35		eqid	⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
36	35	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
37	3 34 36	rspcedvd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } )
38	37	3mix2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
39		3r19.43	⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
40	38 39	sylibr	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
41	27 28	gpgprismgriedgdmel	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )
42	40 41	mpbird	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
43	30 42	prssd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
44		1nn0	⊢ 1 ∈ ℕ₀
45	44	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 1 ∈ ℕ₀ )
46		eluz2gt1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 1 < 𝑁 )
47	13 46	syl	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 1 < 𝑁 )
48		elfzo0	⊢ ( 1 ∈ ( 0 ..^ 𝑁 ) ↔ ( 1 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
49	45 1 47 48	syl3anbrc	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 1 ∈ ( 0 ..^ 𝑁 ) )
50		opeq2	⊢ ( 𝑥 = 1 → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , 1 ⟩ )
51		opeq2	⊢ ( 𝑥 = 1 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 1 ⟩ )
52	50 51	preq12d	⊢ ( 𝑥 = 1 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } )
53	52	eqeq2d	⊢ ( 𝑥 = 1 → ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ) )
54	53	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝑥 = 1 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ) )
55		prcom	⊢ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ }
56	55	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } )
57	49 54 56	rspcedvd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } )
58	57	3mix2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
59		3r19.43	⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
60	58 59	sylibr	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
61	27 28	gpgprismgriedgdmel	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )
62	60 61	mpbird	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
63	8	opeq2d	⊢ ( 𝑥 = 0 → ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 1 mod 𝑁 ) ⟩ )
64	31 63	preq12d	⊢ ( 𝑥 = 0 → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( 1 mod 𝑁 ) ⟩ } )
65	64	eqeq2d	⊢ ( 𝑥 = 0 → ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( 1 mod 𝑁 ) ⟩ } ) )
66	65	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝑥 = 0 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( 1 mod 𝑁 ) ⟩ } ) )
67		prcom	⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ }
68	20	opeq2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ⟨ 1 , 1 ⟩ = ⟨ 1 , ( 1 mod 𝑁 ) ⟩ )
69	68	preq2d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( 1 mod 𝑁 ) ⟩ } )
70	67 69	eqtrid	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( 1 mod 𝑁 ) ⟩ } )
71	3 66 70	rspcedvd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } )
72	71	3mix3d	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
73		3r19.43	⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ↔ ( ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
74	72 73	sylibr	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
75	27 28	gpgprismgriedgdmel	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )
76	74 75	mpbird	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
77	62 76	prssd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
78	43 77	unssd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )

Metamath Proof Explorer

Theorem gpgprismgriedgdmss

Proof