Theorem gpgprismgr4cycllem3

Description: Lemma 3 for gpgprismgr4cycl0 . (Contributed by AV, 5-Nov-2025)

	Ref	Expression
Hypothesis	gpgprismgr4cycllem1.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\}”⟩$$
Assertion	gpgprismgr4cycllem3	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in \left(0..^4\right)\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycllem1.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\}”⟩$$
2		fzo0to42pr	$$⊢\left(0..^4\right)=\left\{0,1\right\}\cup \left\{2,3\right\}$$
3	2	eleq2i	$$⊢X\in \left(0..^4\right)\leftrightarrow X\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\right)$$
4		elun	$$⊢X\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\right)\leftrightarrow \left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)$$
5	3 4	bitri	$$⊢X\in \left(0..^4\right)\leftrightarrow \left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)$$
6		elpri	$$⊢X\in \left\{0,1\right\}\to \left(X=0\vee X=1\right)$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8	7	prid1	$$⊢0\in \left\{0,1\right\}$$
9	8	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left\{0,1\right\}$$
10		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
11		lbfzo0	$$⊢0\in \left(0..^N\right)\leftrightarrow N\in \mathbb{N}$$
12	10 11	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left(0..^N\right)$$
13	9 12	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	14	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in {\mathbb{N}}_0$$
16		uzuzle23	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in {\mathbb{Z}}_{\ge 2}$$
17		eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
18	16 17	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<N$$
19		elfzo0	$$⊢1\in \left(0..^N\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\wedge 1<N\right)$$
20	15 10 18 19	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(0..^N\right)$$
21	9 20	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
22		prelpwi	$$⊢\left(⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
23	13 21 22	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
24		opeq2	$$⊢x=0\to ⟨0,x⟩=⟨0,0⟩$$
25		oveq1	$$⊢x=0\to x+1=0+1$$
26	25	oveq1d	$$⊢x=0\to \left(x+1\right)\mathrm{mod}N=\left(0+1\right)\mathrm{mod}N$$
27	26	opeq2d	$$⊢x=0\to ⟨0,\left(x+1\right)\mathrm{mod}N⟩=⟨0,\left(0+1\right)\mathrm{mod}N⟩$$
28	24 27	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
29	28	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
30		opeq2	$$⊢x=0\to ⟨1,x⟩=⟨1,0⟩$$
31	24 30	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
32	31	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
33	26	opeq2d	$$⊢x=0\to ⟨1,\left(x+1\right)\mathrm{mod}N⟩=⟨1,\left(0+1\right)\mathrm{mod}N⟩$$
34	30 33	preq12d	$$⊢x=0\to \left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
35	34	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
36	29 32 35	3orbi123d	$$⊢x=0\to \left(\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
37		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in ℝ$$
38		1mod	$$⊢\left(N\in ℝ\wedge 1<N\right)\to 1\mathrm{mod}N=1$$
39	37 18 38	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\mathrm{mod}N=1$$
40		1e0p1	$$⊢1=0+1$$
41	40	oveq1i	$$⊢1\mathrm{mod}N=\left(0+1\right)\mathrm{mod}N$$
42	39 41	eqtr3di	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1=\left(0+1\right)\mathrm{mod}N$$
43	42	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,1⟩=⟨0,\left(0+1\right)\mathrm{mod}N⟩$$
44	43	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
45	44	3mix1d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
46	36 12 45	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
47	23 46	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
48		fveq2	$$⊢X=0\to F\left(X\right)=F\left(0\right)$$
49	1	fveq1i	$$⊢F\left(0\right)=⟨“\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\right)$$
50		prex	$$⊢\left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{V}$$
51		s4fv0	$$⊢\left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{V}\to ⟨“\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\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
52	50 51	ax-mp	$$⊢⟨“\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\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
53	49 52	eqtri	$$⊢F\left(0\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
54	48 53	eqtrdi	$$⊢X=0\to F\left(X\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
55	54	eleq1d	$$⊢X=0\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
56	54	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
57	54	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
58	54	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
59	56 57 58	3orbi123d	$$⊢X=0\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
60	59	rexbidv	$$⊢X=0\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
61	55 60	anbi12d	$$⊢X=0\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
62	47 61	imbitrrid	$$⊢X=0\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
63		1ex	$$⊢1\in \mathrm{V}$$
64	63	prid2	$$⊢1\in \left\{0,1\right\}$$
65	64	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left\{0,1\right\}$$
66	65 20	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
67		prelpwi	$$⊢\left(⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
68	21 66 67	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
69		opeq2	$$⊢x=1\to ⟨0,x⟩=⟨0,1⟩$$
70		oveq1	$$⊢x=1\to x+1=1+1$$
71	70	oveq1d	$$⊢x=1\to \left(x+1\right)\mathrm{mod}N=\left(1+1\right)\mathrm{mod}N$$
72	71	opeq2d	$$⊢x=1\to ⟨0,\left(x+1\right)\mathrm{mod}N⟩=⟨0,\left(1+1\right)\mathrm{mod}N⟩$$
73	69 72	preq12d	$$⊢x=1\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}$$
74	73	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
75		opeq2	$$⊢x=1\to ⟨1,x⟩=⟨1,1⟩$$
76	69 75	preq12d	$$⊢x=1\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
77	76	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\right)$$
78	71	opeq2d	$$⊢x=1\to ⟨1,\left(x+1\right)\mathrm{mod}N⟩=⟨1,\left(1+1\right)\mathrm{mod}N⟩$$
79	75 78	preq12d	$$⊢x=1\to \left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}$$
80	79	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
81	74 77 80	3orbi123d	$$⊢x=1\to \left(\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
82		eqid	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
83	82	3mix2i	$$⊢\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
84	83	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
85	81 20 84	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
86	68 85	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
87		fveq2	$$⊢X=1\to F\left(X\right)=F\left(1\right)$$
88	1	fveq1i	$$⊢F\left(1\right)=⟨“\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(1\right)$$
89		prex	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{V}$$
90		s4fv1	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{V}\to ⟨“\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(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
91	89 90	ax-mp	$$⊢⟨“\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(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
92	88 91	eqtri	$$⊢F\left(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
93	87 92	eqtrdi	$$⊢X=1\to F\left(X\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
94	93	eleq1d	$$⊢X=1\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
95	93	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
96	93	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
97	93	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
98	95 96 97	3orbi123d	$$⊢X=1\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
99	98	rexbidv	$$⊢X=1\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
100	94 99	anbi12d	$$⊢X=1\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
101	86 100	imbitrrid	$$⊢X=1\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
102	62 101	jaoi	$$⊢\left(X=0\vee X=1\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
103	6 102	syl	$$⊢X\in \left\{0,1\right\}\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
104		elpri	$$⊢X\in \left\{2,3\right\}\to \left(X=2\vee X=3\right)$$
105	65 12	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
106	66 105	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
107	106	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
108		prelpwi	$$⊢\left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
109	107 108	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
110	28	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
111	31	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
112	34	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
113	110 111 112	3orbi123d	$$⊢x=0\to \left(\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
114		prcom	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1⟩\right\}$$
115	42	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,1⟩=⟨1,\left(0+1\right)\mathrm{mod}N⟩$$
116	115	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨1,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
117	114 116	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
118	117	3mix3d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
119	113 12 118	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
120	119	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
121	109 120	jca	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
122		fveq2	$$⊢X=2\to F\left(X\right)=F\left(2\right)$$
123	1	fveq1i	$$⊢F\left(2\right)=⟨“\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(2\right)$$
124		prex	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}$$
125		s4fv2	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}\to ⟨“\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(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
126	124 125	ax-mp	$$⊢⟨“\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(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
127	123 126	eqtri	$$⊢F\left(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
128	122 127	eqtrdi	$$⊢X=2\to F\left(X\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
129	128	eleq1d	$$⊢X=2\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
130	128	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
131	128	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
132	128	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
133	130 131 132	3orbi123d	$$⊢X=2\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
134	133	rexbidv	$$⊢X=2\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
135	129 134	anbi12d	$$⊢X=2\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
136	135	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
137	121 136	mpbird	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
138	137	expcom	$$⊢X=2\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
139		prelpwi	$$⊢\left(⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
140	105 13 139	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
141	28	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
142	31	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
143	34	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
144	141 142 143	3orbi123d	$$⊢x=0\to \left(\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
145		prcom	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
146	145	3mix2i	$$⊢\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
147	146	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
148	144 12 147	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
149	140 148	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
150		fveq2	$$⊢X=3\to F\left(X\right)=F\left(3\right)$$
151	1	fveq1i	$$⊢F\left(3\right)=⟨“\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(3\right)$$
152		prex	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{V}$$
153		s4fv3	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{V}\to ⟨“\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(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
154	152 153	ax-mp	$$⊢⟨“\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(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
155	151 154	eqtri	$$⊢F\left(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
156	150 155	eqtrdi	$$⊢X=3\to F\left(X\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
157	156	eleq1d	$$⊢X=3\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
158	156	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
159	156	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
160	156	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
161	158 159 160	3orbi123d	$$⊢X=3\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
162	161	rexbidv	$$⊢X=3\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
163	157 162	anbi12d	$$⊢X=3\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
164	149 163	imbitrrid	$$⊢X=3\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
165	138 164	jaoi	$$⊢\left(X=2\vee X=3\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
166	104 165	syl	$$⊢X\in \left\{2,3\right\}\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
167	103 166	jaoi	$$⊢\left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
168	5 167	sylbi	$$⊢X\in \left(0..^4\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
169	168	impcom	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in \left(0..^4\right)\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$