gpgprismgr4cycllem10

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

	Ref	Expression
Hypotheses	gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
	gpgprismgr4cycl.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
	gpgprismgr4cycl.g	No typesetting found for \|- G = ( N gPetersenGr 1 ) with typecode \|-
Assertion	gpgprismgr4cycllem10	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to iEdg (G) (F (X)) = \{P (X), P (X + 1)\}$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
2		gpgprismgr4cycl.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
3		gpgprismgr4cycl.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for \|- G = ( N gPetersenGr 1 ) with typecode \|-
4	3	fveq2i	Could not format ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) : No typesetting found for \|- ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) with typecode \|-
5	4	a1i	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode \|-
6		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
7		1elfzo1ceilhalf1	$⊢ N \in ℤ_{\geq 3} \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
8	6 7	jca	$⊢ N \in ℤ_{\geq 3} \to (N \in ℕ \land 1 \in (1 ..^⌈\frac{N}{2}⌉))$
9	8	adantr	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to (N \in ℕ \land 1 \in (1 ..^⌈\frac{N}{2}⌉))$
10		eqid	$⊢ (1 ..^⌈\frac{N}{2}⌉) = (1 ..^⌈\frac{N}{2}⌉)$
11		eqid	$⊢ (0 ..^N) = (0 ..^N)$
12	10 11	gpgiedg	Could not format ( ( N e. NN /\ 1 e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I \|` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) \| E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ) : No typesetting found for \|- ( ( N e. NN /\ 1 e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I \|` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) \| E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ) with typecode \|-
13	9 12	syl	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I \|` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) \| E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` ( N gPetersenGr 1 ) ) = ( _I \|` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) \| E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) } ) ) with typecode \|-
14	5 13	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to iEdg (G) = {I ↾}_{\{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\}}$
15	14	fveq1d	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to iEdg (G) (F (X)) = ({I ↾}_{\{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\}}) (F (X))$
16	2	gpgprismgr4cycllem3	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^4)) \to (F (X) \in 𝒫 (\{0, 1\} \times (0 ..^N)) \land \exists x \in (0 ..^N) (F (X) = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor F (X) = \{⟨0, x⟩, ⟨1, x⟩\} \lor F (X) = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}))$
17	2	gpgprismgr4cycllem1	$⊢ \|F\| = 4$
18	17	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^4)$
19	18	eleq2i	$⊢ X \in (0 ..^\|F\|) \leftrightarrow X \in (0 ..^4)$
20	19	anbi2i	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \leftrightarrow (N \in ℤ_{\geq 3} \land X \in (0 ..^4))$
21		eqeq1	$⊢ e = F (X) \to (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow F (X) = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\})$
22		eqeq1	$⊢ e = F (X) \to (e = \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow F (X) = \{⟨0, x⟩, ⟨1, x⟩\})$
23		eqeq1	$⊢ e = F (X) \to (e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\} \leftrightarrow F (X) = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})$
24	21 22 23	3orbi123d	$⊢ e = F (X) \to ((e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}) \leftrightarrow (F (X) = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor F (X) = \{⟨0, x⟩, ⟨1, x⟩\} \lor F (X) = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}))$
25	24	rexbidv	$⊢ e = F (X) \to (\exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}) \leftrightarrow \exists x \in (0 ..^N) (F (X) = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor F (X) = \{⟨0, x⟩, ⟨1, x⟩\} \lor F (X) = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}))$
26	25	elrab	$⊢ F (X) \in \{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\} \leftrightarrow (F (X) \in 𝒫 (\{0, 1\} \times (0 ..^N)) \land \exists x \in (0 ..^N) (F (X) = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor F (X) = \{⟨0, x⟩, ⟨1, x⟩\} \lor F (X) = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\}))$
27	16 20 26	3imtr4i	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to F (X) \in \{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\}$
28		fvresi	$⊢ F (X) \in \{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\} \to ({I ↾}_{\{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\}}) (F (X)) = F (X)$
29	27 28	syl	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to ({I ↾}_{\{e \in 𝒫 (\{0, 1\} \times (0 ..^N)) \| \exists x \in (0 ..^N) (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + 1) \mod N⟩\})\}}) (F (X)) = F (X)$
30	15 29	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to iEdg (G) (F (X)) = F (X)$
31		fzo0to42pr	$⊢ (0 ..^4) = \{0, 1\} \cup \{2, 3\}$
32	31	eleq2i	$⊢ X \in (0 ..^4) \leftrightarrow X \in (\{0, 1\} \cup \{2, 3\})$
33		elun	$⊢ X \in (\{0, 1\} \cup \{2, 3\}) \leftrightarrow (X \in \{0, 1\} \lor X \in \{2, 3\})$
34	19 32 33	3bitri	$⊢ X \in (0 ..^\|F\|) \leftrightarrow (X \in \{0, 1\} \lor X \in \{2, 3\})$
35		elpri	$⊢ X \in \{0, 1\} \to (X = 0 \lor X = 1)$
36		prex	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \in V$
37		s4fv0	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \in V \to ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (0) = \{⟨0, 0⟩, ⟨0, 1⟩\}$
38	36 37	ax-mp	$⊢ ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (0) = \{⟨0, 0⟩, ⟨0, 1⟩\}$
39	2	fveq1i	$⊢ F (0) = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (0)$
40	1	fveq1i	$⊢ P (0) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0)$
41		opex	$⊢ ⟨0, 0⟩ \in V$
42		df-s5	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ ++ ⟨“ ⟨0, 0⟩ ”⟩$
43		s4cli	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ \in Word V$
44		s4len	$⊢ \|⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩\| = 4$
45		s4fv0	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
46		0nn0	$⊢ 0 \in ℕ_{0}$
47		4pos	$⊢ 0 < 4$
48	42 43 44 45 46 47	cats1fv	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
49	41 48	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
50	40 49	eqtri	$⊢ P (0) = ⟨0, 0⟩$
51	1	fveq1i	$⊢ P (1) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1)$
52		opex	$⊢ ⟨0, 1⟩ \in V$
53		s4fv1	$⊢ ⟨0, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
54		1nn0	$⊢ 1 \in ℕ_{0}$
55		1lt4	$⊢ 1 < 4$
56	42 43 44 53 54 55	cats1fv	$⊢ ⟨0, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
57	52 56	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
58	51 57	eqtri	$⊢ P (1) = ⟨0, 1⟩$
59	50 58	preq12i	$⊢ \{P (0), P (1)\} = \{⟨0, 0⟩, ⟨0, 1⟩\}$
60	38 39 59	3eqtr4i	$⊢ F (0) = \{P (0), P (1)\}$
61		fveq2	$⊢ X = 0 \to F (X) = F (0)$
62		fveq2	$⊢ X = 0 \to P (X) = P (0)$
63		fv0p1e1	$⊢ X = 0 \to P (X + 1) = P (1)$
64	62 63	preq12d	$⊢ X = 0 \to \{P (X), P (X + 1)\} = \{P (0), P (1)\}$
65	60 61 64	3eqtr4a	$⊢ X = 0 \to F (X) = \{P (X), P (X + 1)\}$
66		prex	$⊢ \{⟨0, 1⟩, ⟨1, 1⟩\} \in V$
67		s4fv1	$⊢ \{⟨0, 1⟩, ⟨1, 1⟩\} \in V \to ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (1) = \{⟨0, 1⟩, ⟨1, 1⟩\}$
68	66 67	ax-mp	$⊢ ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (1) = \{⟨0, 1⟩, ⟨1, 1⟩\}$
69	2	fveq1i	$⊢ F (1) = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (1)$
70	1	fveq1i	$⊢ P (2) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2)$
71		opex	$⊢ ⟨1, 1⟩ \in V$
72		s4fv2	$⊢ ⟨1, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
73		2nn0	$⊢ 2 \in ℕ_{0}$
74		2lt4	$⊢ 2 < 4$
75	42 43 44 72 73 74	cats1fv	$⊢ ⟨1, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
76	71 75	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
77	70 76	eqtri	$⊢ P (2) = ⟨1, 1⟩$
78	58 77	preq12i	$⊢ \{P (1), P (2)\} = \{⟨0, 1⟩, ⟨1, 1⟩\}$
79	68 69 78	3eqtr4i	$⊢ F (1) = \{P (1), P (2)\}$
80		fveq2	$⊢ X = 1 \to F (X) = F (1)$
81		fveq2	$⊢ X = 1 \to P (X) = P (1)$
82		oveq1	$⊢ X = 1 \to X + 1 = 1 + 1$
83		1p1e2	$⊢ 1 + 1 = 2$
84	82 83	eqtrdi	$⊢ X = 1 \to X + 1 = 2$
85	84	fveq2d	$⊢ X = 1 \to P (X + 1) = P (2)$
86	81 85	preq12d	$⊢ X = 1 \to \{P (X), P (X + 1)\} = \{P (1), P (2)\}$
87	79 80 86	3eqtr4a	$⊢ X = 1 \to F (X) = \{P (X), P (X + 1)\}$
88	65 87	jaoi	$⊢ (X = 0 \lor X = 1) \to F (X) = \{P (X), P (X + 1)\}$
89	35 88	syl	$⊢ X \in \{0, 1\} \to F (X) = \{P (X), P (X + 1)\}$
90		elpri	$⊢ X \in \{2, 3\} \to (X = 2 \lor X = 3)$
91		prex	$⊢ \{⟨1, 1⟩, ⟨1, 0⟩\} \in V$
92		s4fv2	$⊢ \{⟨1, 1⟩, ⟨1, 0⟩\} \in V \to ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (2) = \{⟨1, 1⟩, ⟨1, 0⟩\}$
93	91 92	ax-mp	$⊢ ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (2) = \{⟨1, 1⟩, ⟨1, 0⟩\}$
94	2	fveq1i	$⊢ F (2) = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (2)$
95	1	fveq1i	$⊢ P (3) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3)$
96		opex	$⊢ ⟨1, 0⟩ \in V$
97		s4fv3	$⊢ ⟨1, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
98		3nn0	$⊢ 3 \in ℕ_{0}$
99		3lt4	$⊢ 3 < 4$
100	42 43 44 97 98 99	cats1fv	$⊢ ⟨1, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
101	96 100	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
102	95 101	eqtri	$⊢ P (3) = ⟨1, 0⟩$
103	77 102	preq12i	$⊢ \{P (2), P (3)\} = \{⟨1, 1⟩, ⟨1, 0⟩\}$
104	93 94 103	3eqtr4i	$⊢ F (2) = \{P (2), P (3)\}$
105		fveq2	$⊢ X = 2 \to F (X) = F (2)$
106		fveq2	$⊢ X = 2 \to P (X) = P (2)$
107		oveq1	$⊢ X = 2 \to X + 1 = 2 + 1$
108		2p1e3	$⊢ 2 + 1 = 3$
109	107 108	eqtrdi	$⊢ X = 2 \to X + 1 = 3$
110	109	fveq2d	$⊢ X = 2 \to P (X + 1) = P (3)$
111	106 110	preq12d	$⊢ X = 2 \to \{P (X), P (X + 1)\} = \{P (2), P (3)\}$
112	104 105 111	3eqtr4a	$⊢ X = 2 \to F (X) = \{P (X), P (X + 1)\}$
113		prex	$⊢ \{⟨1, 0⟩, ⟨0, 0⟩\} \in V$
114		s4fv3	$⊢ \{⟨1, 0⟩, ⟨0, 0⟩\} \in V \to ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (3) = \{⟨1, 0⟩, ⟨0, 0⟩\}$
115	113 114	ax-mp	$⊢ ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (3) = \{⟨1, 0⟩, ⟨0, 0⟩\}$
116	2	fveq1i	$⊢ F (3) = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ (3)$
117	1	fveq1i	$⊢ P (4) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4)$
118	42 43 44	cats1fvn	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4) = ⟨0, 0⟩$
119	41 118	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4) = ⟨0, 0⟩$
120	117 119	eqtri	$⊢ P (4) = ⟨0, 0⟩$
121	102 120	preq12i	$⊢ \{P (3), P (4)\} = \{⟨1, 0⟩, ⟨0, 0⟩\}$
122	115 116 121	3eqtr4i	$⊢ F (3) = \{P (3), P (4)\}$
123		fveq2	$⊢ X = 3 \to F (X) = F (3)$
124		fveq2	$⊢ X = 3 \to P (X) = P (3)$
125		oveq1	$⊢ X = 3 \to X + 1 = 3 + 1$
126		3p1e4	$⊢ 3 + 1 = 4$
127	125 126	eqtrdi	$⊢ X = 3 \to X + 1 = 4$
128	127	fveq2d	$⊢ X = 3 \to P (X + 1) = P (4)$
129	124 128	preq12d	$⊢ X = 3 \to \{P (X), P (X + 1)\} = \{P (3), P (4)\}$
130	122 123 129	3eqtr4a	$⊢ X = 3 \to F (X) = \{P (X), P (X + 1)\}$
131	112 130	jaoi	$⊢ (X = 2 \lor X = 3) \to F (X) = \{P (X), P (X + 1)\}$
132	90 131	syl	$⊢ X \in \{2, 3\} \to F (X) = \{P (X), P (X + 1)\}$
133	89 132	jaoi	$⊢ (X \in \{0, 1\} \lor X \in \{2, 3\}) \to F (X) = \{P (X), P (X + 1)\}$
134	34 133	sylbi	$⊢ X \in (0 ..^\|F\|) \to F (X) = \{P (X), P (X + 1)\}$
135	134	adantl	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to F (X) = \{P (X), P (X + 1)\}$
136	30 135	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land X \in (0 ..^\|F\|)) \to iEdg (G) (F (X)) = \{P (X), P (X + 1)\}$

Metamath Proof Explorer

Theorem gpgprismgr4cycllem10

Proof