poimirlem14

Description: Lemma for poimir - for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	poimirlem22.s	⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
	poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
Assertion	poimirlem14	⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 ( 2^nd ‘ 𝑧 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		poimirlem22.s	⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
3		poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
4	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 𝑁 ∈ ℕ )
5		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 𝑧 ∈ 𝑆 )
6	1	nngt0d	⊢ ( 𝜑 → 0 < 𝑁 )
7		breq2	⊢ ( ( 2^nd ‘ 𝑧 ) = 𝑁 → ( 0 < ( 2^nd ‘ 𝑧 ) ↔ 0 < 𝑁 ) )
8	7	biimparc	⊢ ( ( 0 < 𝑁 ∧ ( 2^nd ‘ 𝑧 ) = 𝑁 ) → 0 < ( 2^nd ‘ 𝑧 ) )
9	6 8	sylan	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ 𝑧 ) = 𝑁 ) → 0 < ( 2^nd ‘ 𝑧 ) )
10	9	ad2ant2r	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 0 < ( 2^nd ‘ 𝑧 ) )
11	4 2 5 10	poimirlem5	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 𝐹 ‘ 0 ) = ( 1^st ‘ ( 1^st ‘ 𝑧 ) ) )
12		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 𝑘 ∈ 𝑆 )
13		breq2	⊢ ( ( 2^nd ‘ 𝑘 ) = 𝑁 → ( 0 < ( 2^nd ‘ 𝑘 ) ↔ 0 < 𝑁 ) )
14	13	biimparc	⊢ ( ( 0 < 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → 0 < ( 2^nd ‘ 𝑘 ) )
15	6 14	sylan	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → 0 < ( 2^nd ‘ 𝑘 ) )
16	15	ad2ant2rl	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 0 < ( 2^nd ‘ 𝑘 ) )
17	4 2 12 16	poimirlem5	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 𝐹 ‘ 0 ) = ( 1^st ‘ ( 1^st ‘ 𝑘 ) ) )
18	11 17	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑧 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑘 ) ) )
19		elrabi	⊢ ( 𝑧 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
20	19 2	eleq2s	⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
21		xp1st	⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
22		xp2nd	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
23	20 21 22	3syl	⊢ ( 𝑧 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
24		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ∈ V
25		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
26	24 25	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
27	23 26	sylib	⊢ ( 𝑧 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
28		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) )
29	27 28	syl	⊢ ( 𝑧 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) )
30	29	adantr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) )
31	30	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) )
32		elrabi	⊢ ( 𝑘 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑘 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
33	32 2	eleq2s	⊢ ( 𝑘 ∈ 𝑆 → 𝑘 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
34		xp1st	⊢ ( 𝑘 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑘 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
35		xp2nd	⊢ ( ( 1^st ‘ 𝑘 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
36	33 34 35	3syl	⊢ ( 𝑘 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
37		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ∈ V
38		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
39	37 38	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
40	36 39	sylib	⊢ ( 𝑘 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
41		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
42	40 41	syl	⊢ ( 𝑘 ∈ 𝑆 → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
43	42	adantl	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
44	43	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
45		simpllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) )
46		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
47	46	imaeq2d	⊢ ( 𝑛 = 𝑁 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) )
48		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
49		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
50	27 48 49	3syl	⊢ ( 𝑧 ∈ 𝑆 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
51	47 50	sylan9eqr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑁 ) )
52	51	adantlr	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑁 ) )
53	46	imaeq2d	⊢ ( 𝑛 = 𝑁 → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) )
54		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
55		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
56	40 54 55	3syl	⊢ ( 𝑘 ∈ 𝑆 → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
57	53 56	sylan9eqr	⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑁 ) )
58	57	adantll	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑁 ) )
59	52 58	eqtr4d	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
60	45 59	sylan	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
61		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 𝜑 )
62		elnnuz	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ_≥ ‘ 1 ) )
63	1 62	sylib	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 1 ) )
64		fzm1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 1 ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ) )
65	63 64	syl	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ) )
66	65	anbi1d	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ↔ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) )
67	66	biimpa	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) )
68		df-ne	⊢ ( 𝑛 ≠ 𝑁 ↔ ¬ 𝑛 = 𝑁 )
69	68	anbi2i	⊢ ( ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ↔ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ ¬ 𝑛 = 𝑁 ) )
70		pm5.61	⊢ ( ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ ¬ 𝑛 = 𝑁 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ¬ 𝑛 = 𝑁 ) )
71	69 70	bitri	⊢ ( ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑛 = 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ↔ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ¬ 𝑛 = 𝑁 ) )
72	67 71	sylib	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ¬ 𝑛 = 𝑁 ) )
73		fz1ssfz0	⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) )
74	73	sseli	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
75	74	adantr	⊢ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ¬ 𝑛 = 𝑁 ) → 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
76	72 75	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) → 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
77	61 76	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) → 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
78		eleq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
79	78	anbi2d	⊢ ( 𝑚 = 𝑛 → ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
80		oveq2	⊢ ( 𝑚 = 𝑛 → ( 1 ... 𝑚 ) = ( 1 ... 𝑛 ) )
81	80	imaeq2d	⊢ ( 𝑚 = 𝑛 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) )
82	80	imaeq2d	⊢ ( 𝑚 = 𝑛 → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
83	81 82	eqeq12d	⊢ ( 𝑚 = 𝑛 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ) )
84	79 83	imbi12d	⊢ ( 𝑚 = 𝑛 → ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ) ) )
85	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
86	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
87		simpl	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
88	87	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑧 ∈ 𝑆 )
89		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑧 ) = 𝑁 )
90		simpr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ 𝑆 )
91	90	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ 𝑆 )
92		simplrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑘 ) = 𝑁 )
93		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
94	85 2 86 88 89 91 92 93	poimirlem12	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) )
95	85 2 86 91 92 88 89 93	poimirlem12	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) ⊆ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) )
96	94 95	eqssd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) )
97	84 96	chvarvv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
98	77 97	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
99	98	anassrs	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑛 ≠ 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
100	60 99	pm2.61dane	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
101		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
102		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℤ )
103	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
104		elfzm1b	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
105	102 103 104	syl2anr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
106	101 105	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
107	61 106	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
108		ovex	⊢ ( 𝑛 − 1 ) ∈ V
109		eleq1	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
110	109	anbi2d	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
111		oveq2	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 1 ... 𝑚 ) = ( 1 ... ( 𝑛 − 1 ) ) )
112	111	imaeq2d	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) )
113	111	imaeq2d	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) )
114	112 113	eqeq12d	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
115	110 114	imbi12d	⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑚 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑚 ) ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) ) )
116	108 115 96	vtocl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) )
117	107 116	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) )
118	100 117	difeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
119		fnsnfv	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ { 𝑛 } ) )
120	29 119	sylan	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ { 𝑛 } ) )
121		elfznn	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℕ )
122		uncom	⊢ ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) = ( { 𝑛 } ∪ ( 1 ... ( 𝑛 − 1 ) ) )
123	122	difeq1i	⊢ ( ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( { 𝑛 } ∪ ( 1 ... ( 𝑛 − 1 ) ) ) ∖ ( 1 ... ( 𝑛 − 1 ) ) )
124		difun2	⊢ ( ( { 𝑛 } ∪ ( 1 ... ( 𝑛 − 1 ) ) ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = ( { 𝑛 } ∖ ( 1 ... ( 𝑛 − 1 ) ) )
125	123 124	eqtri	⊢ ( ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = ( { 𝑛 } ∖ ( 1 ... ( 𝑛 − 1 ) ) )
126		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
127		npcan1	⊢ ( 𝑛 ∈ ℂ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
128	126 127	syl	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
129		elnnuz	⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
130	129	biimpi	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
131	128 130	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
132		nnm1nn0	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ₀ )
133	132	nn0zd	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℤ )
134		uzid	⊢ ( ( 𝑛 − 1 ) ∈ ℤ → ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) )
135		peano2uz	⊢ ( ( 𝑛 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) )
136	133 134 135	3syl	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) )
137	128 136	eqeltrrd	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) )
138		fzsplit2	⊢ ( ( ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ ( 𝑛 − 1 ) ) ) → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) )
139	131 137 138	syl2anc	⊢ ( 𝑛 ∈ ℕ → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) )
140	128	oveq1d	⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) = ( 𝑛 ... 𝑛 ) )
141		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
142		fzsn	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ... 𝑛 ) = { 𝑛 } )
143	141 142	syl	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ... 𝑛 ) = { 𝑛 } )
144	140 143	eqtrd	⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) = { 𝑛 } )
145	144	uneq2d	⊢ ( 𝑛 ∈ ℕ → ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) )
146	139 145	eqtrd	⊢ ( 𝑛 ∈ ℕ → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) )
147	146	difeq1d	⊢ ( 𝑛 ∈ ℕ → ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) )
148		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
149		ltm1	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) < 𝑛 )
150		peano2rem	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
151		ltnle	⊢ ( ( ( 𝑛 − 1 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 𝑛 − 1 ) < 𝑛 ↔ ¬ 𝑛 ≤ ( 𝑛 − 1 ) ) )
152	150 151	mpancom	⊢ ( 𝑛 ∈ ℝ → ( ( 𝑛 − 1 ) < 𝑛 ↔ ¬ 𝑛 ≤ ( 𝑛 − 1 ) ) )
153	149 152	mpbid	⊢ ( 𝑛 ∈ ℝ → ¬ 𝑛 ≤ ( 𝑛 − 1 ) )
154		elfzle2	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑛 − 1 ) ) → 𝑛 ≤ ( 𝑛 − 1 ) )
155	153 154	nsyl	⊢ ( 𝑛 ∈ ℝ → ¬ 𝑛 ∈ ( 1 ... ( 𝑛 − 1 ) ) )
156	148 155	syl	⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 ∈ ( 1 ... ( 𝑛 − 1 ) ) )
157		incom	⊢ ( ( 1 ... ( 𝑛 − 1 ) ) ∩ { 𝑛 } ) = ( { 𝑛 } ∩ ( 1 ... ( 𝑛 − 1 ) ) )
158	157	eqeq1i	⊢ ( ( ( 1 ... ( 𝑛 − 1 ) ) ∩ { 𝑛 } ) = ∅ ↔ ( { 𝑛 } ∩ ( 1 ... ( 𝑛 − 1 ) ) ) = ∅ )
159		disjsn	⊢ ( ( ( 1 ... ( 𝑛 − 1 ) ) ∩ { 𝑛 } ) = ∅ ↔ ¬ 𝑛 ∈ ( 1 ... ( 𝑛 − 1 ) ) )
160		disj3	⊢ ( ( { 𝑛 } ∩ ( 1 ... ( 𝑛 − 1 ) ) ) = ∅ ↔ { 𝑛 } = ( { 𝑛 } ∖ ( 1 ... ( 𝑛 − 1 ) ) ) )
161	158 159 160	3bitr3i	⊢ ( ¬ 𝑛 ∈ ( 1 ... ( 𝑛 − 1 ) ) ↔ { 𝑛 } = ( { 𝑛 } ∖ ( 1 ... ( 𝑛 − 1 ) ) ) )
162	156 161	sylib	⊢ ( 𝑛 ∈ ℕ → { 𝑛 } = ( { 𝑛 } ∖ ( 1 ... ( 𝑛 − 1 ) ) ) )
163	125 147 162	3eqtr4a	⊢ ( 𝑛 ∈ ℕ → ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = { 𝑛 } )
164	121 163	syl	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) = { 𝑛 } )
165	164	imaeq2d	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ { 𝑛 } ) )
166	165	adantl	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ { 𝑛 } ) )
167		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ) )
168	167	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) )
169		imadif	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
170	27 168 169	3syl	⊢ ( 𝑧 ∈ 𝑆 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
171	170	adantr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( ( 1 ... 𝑛 ) ∖ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
172	120 166 171	3eqtr2d	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
173	5 172	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
174		eleq1	⊢ ( 𝑧 = 𝑘 → ( 𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆 ) )
175	174	anbi1d	⊢ ( 𝑧 = 𝑘 → ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) )
176		2fveq3	⊢ ( 𝑧 = 𝑘 → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) )
177	176	fveq1d	⊢ ( 𝑧 = 𝑘 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) )
178	177	sneqd	⊢ ( 𝑧 = 𝑘 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } )
179	176	imaeq1d	⊢ ( 𝑧 = 𝑘 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) )
180	176	imaeq1d	⊢ ( 𝑧 = 𝑘 → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) )
181	179 180	difeq12d	⊢ ( 𝑧 = 𝑘 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
182	178 181	eqeq12d	⊢ ( 𝑧 = 𝑘 → ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) ↔ { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) ) )
183	175 182	imbi12d	⊢ ( 𝑧 = 𝑘 → ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) ) ↔ ( ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) ) ) )
184	183 172	chvarvv	⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
185	12 184	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... 𝑛 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) “ ( 1 ... ( 𝑛 − 1 ) ) ) ) )
186	118 173 185	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } )
187		fvex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ V
188	187	sneqr	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) } → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) )
189	186 188	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ‘ 𝑛 ) )
190	31 44 189	eqfnfvd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) )
191	20 21	syl	⊢ ( 𝑧 ∈ 𝑆 → ( 1^st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
192	33 34	syl	⊢ ( 𝑘 ∈ 𝑆 → ( 1^st ‘ 𝑘 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
193		xpopth	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ ( 1^st ‘ 𝑘 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑧 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ) ↔ ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ) )
194	191 192 193	syl2an	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑧 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ) ↔ ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ) )
195	194	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑧 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑘 ) ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑘 ) ) ) ↔ ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ) )
196	18 190 195	mpbi2and	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) )
197		eqtr3	⊢ ( ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑘 ) )
198	197	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑘 ) )
199		xpopth	⊢ ( ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ) → ( ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑘 ) ) ↔ 𝑧 = 𝑘 ) )
200	20 33 199	syl2an	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑘 ) ) ↔ 𝑧 = 𝑘 ) )
201	200	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → ( ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑘 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑘 ) ) ↔ 𝑧 = 𝑘 ) )
202	196 198 201	mpbi2and	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ∧ ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) ) → 𝑧 = 𝑘 )
203	202	ex	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → ( ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → 𝑧 = 𝑘 ) )
204	203	ralrimivva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 ( ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → 𝑧 = 𝑘 ) )
205		fveqeq2	⊢ ( 𝑧 = 𝑘 → ( ( 2^nd ‘ 𝑧 ) = 𝑁 ↔ ( 2^nd ‘ 𝑘 ) = 𝑁 ) )
206	205	rmo4	⊢ ( ∃* 𝑧 ∈ 𝑆 ( 2^nd ‘ 𝑧 ) = 𝑁 ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 ( ( ( 2^nd ‘ 𝑧 ) = 𝑁 ∧ ( 2^nd ‘ 𝑘 ) = 𝑁 ) → 𝑧 = 𝑘 ) )
207	204 206	sylibr	⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 ( 2^nd ‘ 𝑧 ) = 𝑁 )

Metamath Proof Explorer

Theorem poimirlem14

Proof