Theorem axlowdim

Description: The general lower dimension axiom. Take a dimension N greater than or equal to three. Then, there are three non-colinear points in N dimensional space that are equidistant from N - 1 distinct points. Derived from remarks inTarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013)

	Ref	Expression
Assertion	axlowdim	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzuzle23	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
2		0re	⊢ 0 ∈ ℝ
3	2 2	axlowdimlem5	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
4	1 3	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
5		1re	⊢ 1 ∈ ℝ
6	5 2	axlowdimlem5	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
7	1 6	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
8	2 5	axlowdimlem5	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
9	1 8	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
10		eqid	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) )
11	10	axlowdimlem15	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) )
12		eqid	⊢ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
13		eqid	⊢ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) = ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) )
14		eqid	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
15	12 13 14 2 2	axlowdimlem17	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
16		eqid	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
17	12 13 16 5 2	axlowdimlem17	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
18		eqid	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
19	12 13 18 2 5	axlowdimlem17	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
20		1zzd	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 1 ∈ ℤ )
21		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
22	21	3ad2ant2	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℤ )
23		2m1e1	⊢ ( 2 − 1 ) = 1
24		2re	⊢ 2 ∈ ℝ
25		3re	⊢ 3 ∈ ℝ
26		2lt3	⊢ 2 < 3
27	24 25 26	ltleii	⊢ 2 ≤ 3
28		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
29		letr	⊢ ( ( 2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 2 ≤ 3 ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 ) )
30	24 25 28 29	mp3an12i	⊢ ( 𝑁 ∈ ℤ → ( ( 2 ≤ 3 ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 ) )
31	27 30	mpani	⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 → 2 ≤ 𝑁 ) )
32	31	imp	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 )
33	32	3adant1	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 ≤ 𝑁 )
34	28	3ad2ant2	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
35		lesub1	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) ≤ ( 𝑁 − 1 ) ) )
36	24 5 35	mp3an13	⊢ ( 𝑁 ∈ ℝ → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) ≤ ( 𝑁 − 1 ) ) )
37	34 36	syl	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) ≤ ( 𝑁 − 1 ) ) )
38	33 37	mpbid	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → ( 2 − 1 ) ≤ ( 𝑁 − 1 ) )
39	23 38	eqbrtrrid	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 1 ≤ ( 𝑁 − 1 ) )
40	20 22 39	3jca	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑁 − 1 ) ) )
41		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) )
42		eluz2	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑁 − 1 ) ) )
43	40 41 42	3imtr4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
44		eluzfz1	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
45	43 44	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
46	45	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
47		eqeq1	⊢ ( 𝑘 = 1 → ( 𝑘 = 1 ↔ 1 = 1 ) )
48		oveq1	⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
49	48	opeq1d	⊢ ( 𝑘 = 1 → ⟨ ( 𝑘 + 1 ) , 1 ⟩ = ⟨ ( 1 + 1 ) , 1 ⟩ )
50	49	sneqd	⊢ ( 𝑘 = 1 → { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } = { ⟨ ( 1 + 1 ) , 1 ⟩ } )
51	48	sneqd	⊢ ( 𝑘 = 1 → { ( 𝑘 + 1 ) } = { ( 1 + 1 ) } )
52	51	difeq2d	⊢ ( 𝑘 = 1 → ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) = ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) )
53	52	xpeq1d	⊢ ( 𝑘 = 1 → ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) = ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) )
54	50 53	uneq12d	⊢ ( 𝑘 = 1 → ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) = ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) )
55	47 54	ifbieq2d	⊢ ( 𝑘 = 1 → if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) = if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) )
56		snex	⊢ { ⟨ 3 , - 1 ⟩ } ∈ V
57		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
58	57	difexi	⊢ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ∈ V
59		snex	⊢ { 0 } ∈ V
60	58 59	xpex	⊢ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ∈ V
61	56 60	unex	⊢ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) ∈ V
62		snex	⊢ { ⟨ ( 1 + 1 ) , 1 ⟩ } ∈ V
63	57	difexi	⊢ ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) ∈ V
64	63 59	xpex	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ∈ V
65	62 64	unex	⊢ ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ∈ V
66	61 65	ifex	⊢ if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) ∈ V
67	55 10 66	fvmpt	⊢ ( 1 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) = if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) )
68	46 67	syl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) = if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) )
69		eqid	⊢ 1 = 1
70	69	iftruei	⊢ if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
71	68 70	eqtrdi	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) )
72	71	opeq1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
73		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
74		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
75	73 74	ax-mp	⊢ ( 2 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) )
76	75	sseli	⊢ ( 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
77	76	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
78		eqeq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 = 1 ↔ 𝑖 = 1 ) )
79		oveq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 + 1 ) = ( 𝑖 + 1 ) )
80	79	opeq1d	⊢ ( 𝑘 = 𝑖 → ⟨ ( 𝑘 + 1 ) , 1 ⟩ = ⟨ ( 𝑖 + 1 ) , 1 ⟩ )
81	80	sneqd	⊢ ( 𝑘 = 𝑖 → { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } = { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } )
82	79	sneqd	⊢ ( 𝑘 = 𝑖 → { ( 𝑘 + 1 ) } = { ( 𝑖 + 1 ) } )
83	82	difeq2d	⊢ ( 𝑘 = 𝑖 → ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) = ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) )
84	83	xpeq1d	⊢ ( 𝑘 = 𝑖 → ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) = ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) )
85	81 84	uneq12d	⊢ ( 𝑘 = 𝑖 → ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) = ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) )
86	78 85	ifbieq2d	⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) = if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) )
87		snex	⊢ { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∈ V
88	57	difexi	⊢ ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) ∈ V
89	88 59	xpex	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ∈ V
90	87 89	unex	⊢ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ∈ V
91	61 90	ifex	⊢ if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) ∈ V
92	86 10 91	fvmpt	⊢ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) )
93	77 92	syl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) )
94		1lt2	⊢ 1 < 2
95	5 24	ltnlei	⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
96	94 95	mpbi	⊢ ¬ 2 ≤ 1
97	96	intnanr	⊢ ¬ ( 2 ≤ 1 ∧ 1 ≤ ( 𝑁 − 1 ) )
98		1z	⊢ 1 ∈ ℤ
99		2z	⊢ 2 ∈ ℤ
100		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
101	100 21	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) ∈ ℤ )
102		elfz	⊢ ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 1 ∈ ( 2 ... ( 𝑁 − 1 ) ) ↔ ( 2 ≤ 1 ∧ 1 ≤ ( 𝑁 − 1 ) ) ) )
103	98 99 101 102	mp3an12i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ∈ ( 2 ... ( 𝑁 − 1 ) ) ↔ ( 2 ≤ 1 ∧ 1 ≤ ( 𝑁 − 1 ) ) ) )
104	97 103	mtbiri	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ 1 ∈ ( 2 ... ( 𝑁 − 1 ) ) )
105		eleq1	⊢ ( 𝑖 = 1 → ( 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ↔ 1 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) )
106	105	notbid	⊢ ( 𝑖 = 1 → ( ¬ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ↔ ¬ 1 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) )
107	104 106	syl5ibrcom	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑖 = 1 → ¬ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) )
108	107	con2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) → ¬ 𝑖 = 1 ) )
109	108	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑖 = 1 )
110	109	iffalsed	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) = ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) )
111	93 110	eqtrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) = ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) )
112	111	opeq1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
113	72 112	breq12d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
114	71	opeq1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
115	111	opeq1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
116	114 115	breq12d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
117	45 67	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) = if ( 1 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 1 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 1 + 1 ) } ) × { 0 } ) ) ) )
118	117 70	eqtrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) )
119	118	opeq1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
120	119	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
121	111	opeq1d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
122	120 121	breq12d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
123	113 116 122	3anbi123d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ↔ ( ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
124	15 17 19 123	mpbir3and	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
125	124	ralrimiva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
126	14 16 18	axlowdimlem6	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
127	1 126	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
128		opeq2	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
129		opeq2	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
130	128 129	breq12d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
131	130	3anbi1d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
132	131	ralbidv	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
133		breq1	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ) )
134		opeq2	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑧 , 𝑥 ⟩ = ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
135	134	breq2d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ↔ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
136		opeq1	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ )
137	136	breq2d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) )
138	133 135 137	3orbi123d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) )
139	138	notbid	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) )
140	132 139	3anbi23d	⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) ) )
141		opeq2	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
142		opeq2	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
143	141 142	breq12d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
144	143	3anbi2d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
145	144	ralbidv	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
146		opeq1	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ )
147	146	breq2d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ) )
148		breq1	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
149		opeq2	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
150	149	breq2d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
151	147 148 150	3orbi123d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
152	151	notbid	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
153	145 152	3anbi23d	⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) ) )
154		opeq2	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
155		opeq2	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
156	154 155	breq12d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
157	156	3anbi3d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
158	157	ralbidv	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
159		opeq2	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ = ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
160	159	breq2d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
161		opeq1	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
162	161	breq2d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
163		breq1	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
164	160 162 163	3orbi123d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
165	164	notbid	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
166	158 165	3anbi23d	⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) ) )
167	140 153 166	rspc3ev	⊢ ( ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )
168	4 7 9 11 125 127 167	syl33anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )
169		ovex	⊢ ( 1 ... ( 𝑁 − 1 ) ) ∈ V
170	169	mptex	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ∈ V
171		f1eq1	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ) )
172		fveq1	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( 𝑝 ‘ 1 ) = ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) )
173	172	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ )
174		fveq1	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) )
175	174	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ )
176	173 175	breq12d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ) )
177	172	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ )
178	174	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ )
179	177 178	breq12d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ) )
180	172	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ )
181	174	opeq1d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ = ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ )
182	180 181	breq12d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ↔ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) )
183	176 179 182	3anbi123d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
184	183	ralbidv	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ↔ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ) )
185	171 184	3anbi12d	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
186	185	rexbidv	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
187	186	2rexbidv	⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
188	170 187	spcev	⊢ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑘 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑘 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑘 + 1 ) } ) × { 0 } ) ) ) ) ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑝 ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )
189	168 188	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑝 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑁 − 1 ) ) ( ⟨ ( 𝑝 ‘ 1 ) , 𝑥 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑥 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑦 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑦 ⟩ ∧ ⟨ ( 𝑝 ‘ 1 ) , 𝑧 ⟩ Cgr ⟨ ( 𝑝 ‘ 𝑖 ) , 𝑧 ⟩ ) ∧ ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )