poimirlem13

Description: Lemma for poimir - for at most one simplex associated with a shared face is the opposite vertex first 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	poimirlem13	⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 ( 2^nd ‘ 𝑧 ) = 0 )

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

Metamath Proof Explorer

Theorem poimirlem13

Proof