poimirlem17

	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 ... 𝑁 ) ) )
	poimirlem22.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem18.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
	poimirlem18.4	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 0 )
Assertion	poimirlem17	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

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		poimirlem22.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		poimirlem18.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
6		poimirlem18.4	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 0 )
7	1 2 3 4 5 6	poimirlem16	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
8		elfznn0	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℕ₀ )
9	8	nn0red	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℝ )
11	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
13	11 12	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
14	13	zred	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
16	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
18		elfzle2	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
20	16	ltm1d	⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
22	10 15 17 19 21	lelttrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < 𝑁 )
23	22	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < 𝑁 )
24		fveq2	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) )
25		opex	⊢ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ∈ V
26		op2ndg	⊢ ( ( ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ∈ V ∧ 𝑁 ∈ ℕ ) → ( 2^nd ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) = 𝑁 )
27	25 1 26	sylancr	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) = 𝑁 )
28	24 27	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 2^nd ‘ 𝑡 ) = 𝑁 )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑡 ) = 𝑁 )
30	23 29	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < ( 2^nd ‘ 𝑡 ) )
31	30	iftrued	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
32	31	csbeq1d	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑦 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
33		vex	⊢ 𝑦 ∈ V
34		oveq2	⊢ ( 𝑗 = 𝑦 → ( 1 ... 𝑗 ) = ( 1 ... 𝑦 ) )
35	34	imaeq2d	⊢ ( 𝑗 = 𝑦 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) )
36	35	xpeq1d	⊢ ( 𝑗 = 𝑦 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
37		oveq1	⊢ ( 𝑗 = 𝑦 → ( 𝑗 + 1 ) = ( 𝑦 + 1 ) )
38	37	oveq1d	⊢ ( 𝑗 = 𝑦 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
39	38	imaeq2d	⊢ ( 𝑗 = 𝑦 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
40	39	xpeq1d	⊢ ( 𝑗 = 𝑦 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
41	36 40	uneq12d	⊢ ( 𝑗 = 𝑦 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
42	41	oveq2d	⊢ ( 𝑗 = 𝑦 → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
43	33 42	csbie	⊢ ⦋ 𝑦 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
44		2fveq3	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ) )
45		op1stg	⊢ ( ( ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ∈ V ∧ 𝑁 ∈ ℕ ) → ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ )
46	25 1 45	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ )
47	46	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ) = ( 1^st ‘ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ) )
48		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
49	48	mptex	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∈ V
50		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ V
51	48	mptex	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ∈ V
52	50 51	coex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ∈ V
53	49 52	op1st	⊢ ( 1^st ‘ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) )
54	47 53	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) )
55	44 54	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) )
56		fveq2	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 1^st ‘ 𝑡 ) = ( 1^st ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) )
57	56 46	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 1^st ‘ 𝑡 ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ )
58	57	fveq2d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ) )
59	49 52	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) )
60	58 59	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) )
61	60	imaeq1d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) )
62	61	xpeq1d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
63	60	imaeq1d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
64	63	xpeq1d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
65	62 64	uneq12d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
66	55 65	oveq12d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
67	43 66	syl5eq	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ⦋ 𝑦 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
68	67	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ 𝑦 / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
69	32 68	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
70	69	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
71	70	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
72	71	ex	⊢ ( 𝜑 → ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) ) )
73	72	alrimiv	⊢ ( 𝜑 → ∀ 𝑡 ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) ) )
74		oveq2	⊢ ( 1 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) )
75	74	eleq1d	⊢ ( 1 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) ) )
76		oveq2	⊢ ( 0 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 0 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) )
77	76	eleq1d	⊢ ( 0 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 0 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) ) )
78		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
79	78	oveq1d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
80	79	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
81		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 ... 𝑁 ) ) )
82	81 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
83		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
84	4 82 83	3syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
85		xp1st	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
86		elmapi	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
87	84 85 86	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
88	4 82	syl	⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
89		xp2nd	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
90	88 83 89	3syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
91		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
92	50 91	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
93	90 92	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
94		f1of	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
95	93 94	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
96		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
97	1 96	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 1 ) )
98		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
99	97 98	syl	⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑁 ) )
100	95 99	ffvelrnd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) )
101	87 100	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ( 0 ..^ 𝐾 ) )
102		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℕ₀ )
103		peano2nn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℕ₀ → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ℕ₀ )
104	101 102 103	3syl	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ℕ₀ )
105		elfzo0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 ) )
106	101 105	sylib	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 ) )
107	106	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
108	104	nn0red	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ℝ )
109	107	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
110		elfzolt2	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 )
111	101 110	syl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 )
112	101 102	syl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℕ₀ )
113	112	nn0zd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℤ )
114	107	nnzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
115		zltp1le	⊢ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ≤ 𝐾 ) )
116	113 114 115	syl2anc	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) < 𝐾 ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ≤ 𝐾 ) )
117	111 116	mpbid	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ≤ 𝐾 )
118		fvex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ V
119		eleq1	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) )
120	119	anbi2d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) ) )
121		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( 𝑝 ‘ 𝑛 ) = ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
122	121	neeq1d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 ↔ ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 ) )
123	122	rexbidv	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 ↔ ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 ) )
124	120 123	imbi12d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 ) ↔ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 ) ) )
125	118 124 5	vtocl	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 )
126	100 125	mpdan	⊢ ( 𝜑 → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 )
127		fveq1	⊢ ( 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
128	87	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
129	128	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
130		1ex	⊢ 1 ∈ V
131		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
132	130 131	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) )
133		c0ex	⊢ 0 ∈ V
134		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
135	133 134	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
136	132 135	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
137		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
138	137	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
139		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) )
140	93 138 139	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) )
141		nn0p1nn	⊢ ( 𝑦 ∈ ℕ₀ → ( 𝑦 + 1 ) ∈ ℕ )
142	8 141	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℕ )
143	142	nnred	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℝ )
144	143	ltp1d	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) < ( ( 𝑦 + 1 ) + 1 ) )
145		fzdisj	⊢ ( ( 𝑦 + 1 ) < ( ( 𝑦 + 1 ) + 1 ) → ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
146	145	imaeq2d	⊢ ( ( 𝑦 + 1 ) < ( ( 𝑦 + 1 ) + 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
147		ima0	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) = ∅
148	146 147	eqtrdi	⊢ ( ( 𝑦 + 1 ) < ( ( 𝑦 + 1 ) + 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
149	144 148	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
150	140 149	sylan9req	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
151		fnun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) )
152	136 150 151	sylancr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) )
153		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
154	142	peano2nnd	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℕ )
155	154 96	eleqtrdi	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
156	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
157		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
158	156 157	syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
159	158	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
160		elfzuz3	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) )
161		eluzp1p1	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
162	160 161	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
163	162	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
164	159 163	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
165		fzsplit2	⊢ ( ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
166	155 164 165	syl2an2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
167	166	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) )
168		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
169		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
170	93 168 169	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
171	170	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
172	167 171	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
173	153 172	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
174	173	fneq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
175	152 174	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
176	48	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) ∈ V )
177		inidm	⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
178		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
179		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
180	93 179	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
181	180	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
182		fzss2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
183	164 182	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
184	142 96	eleqtrdi	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
185		eluzfz1	⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) → 1 ∈ ( 1 ... ( 𝑦 + 1 ) ) )
186	184 185	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 1 ∈ ( 1 ... ( 𝑦 + 1 ) ) )
187	186	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ( 1 ... ( 𝑦 + 1 ) ) )
188		fnfvima	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) ∧ 1 ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
189	181 183 187 188	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
190		fvun1	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
191	132 135 190	mp3an12	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
192	150 189 191	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) )
193	130	fvconst2	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 1 )
194	189 193	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 1 )
195	192 194	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 1 )
196	195	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 1 )
197	129 175 176 176 177 178 196	ofval	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
198	100 197	mpidan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
199	127 198	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
200	199	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
201		fveq2	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑇 ) )
202	201	breq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
203	202	ifbid	⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
204		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
205		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
206	205	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
207	206	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
208	205	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
209	208	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
210	207 209	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
211	204 210	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
212	203 211	csbeq12dv	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
213	212	mpteq2dv	⊢ ( 𝑡 = 𝑇 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 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 } ) ) ) ) )
214	213	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 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 } ) ) ) ) ) )
215	214 2	elrab2	⊢ ( 𝑇 ∈ 𝑆 ↔ ( 𝑇 ∈ ( ( ( ( 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 } ) ) ) ) ) )
216	215	simprbi	⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
217	4 216	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
218	217	rneqd	⊢ ( 𝜑 → ran 𝐹 = ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
219	218	eleq2d	⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
220		eqid	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 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 } ) ) ) )
221		ovex	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
222	221	csbex	⊢ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
223	220 222	elrnmpti	⊢ ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 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 } ) ) ) )
224	219 223	bitrdi	⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
225	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑇 ) = 0 )
226		elfzle1	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 0 ≤ 𝑦 )
227	226	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 0 ≤ 𝑦 )
228	225 227	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑇 ) ≤ 𝑦 )
229		0re	⊢ 0 ∈ ℝ
230	6 229	eqeltrdi	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℝ )
231		lenlt	⊢ ( ( ( 2^nd ‘ 𝑇 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 2^nd ‘ 𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
232	230 9 231	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ 𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
233	228 232	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑦 < ( 2^nd ‘ 𝑇 ) )
234	233	iffalsed	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
235	234	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
236		ovex	⊢ ( 𝑦 + 1 ) ∈ V
237		oveq2	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑦 + 1 ) ) )
238	237	imaeq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
239	238	xpeq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
240		oveq1	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
241	240	oveq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
242	241	imaeq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
243	242	xpeq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
244	239 243	uneq12d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
245	244	oveq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
246	236 245	csbie	⊢ ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
247	235 246	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
248	247	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑝 = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ↔ 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
249	248	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
250	224 249	bitrd	⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
251	250	biimpa	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
252	200 251	r19.29a	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
253		eqtr3	⊢ ( ( ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∧ 𝐾 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 𝐾 )
254	253	ex	⊢ ( ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) → ( 𝐾 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 𝐾 ) )
255	252 254	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( 𝐾 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) = 𝐾 ) )
256	255	necon3d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 → 𝐾 ≠ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ) )
257	256	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) ≠ 𝐾 → 𝐾 ≠ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ) )
258	126 257	mpd	⊢ ( 𝜑 → 𝐾 ≠ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) )
259	108 109 117 258	leneltd	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) < 𝐾 )
260		elfzo0	⊢ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) < 𝐾 ) )
261	104 107 259 260	syl3anbrc	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ( 0 ..^ 𝐾 ) )
262	261	adantr	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) + 1 ) ∈ ( 0 ..^ 𝐾 ) )
263	80 262	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) ∈ ( 0 ..^ 𝐾 ) )
264	263	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 1 ) ∈ ( 0 ..^ 𝐾 ) )
265	87	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) )
266		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℕ₀ )
267	265 266	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℕ₀ )
268	267	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℂ )
269	268	addid1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) )
270	269 265	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 0 ) ∈ ( 0 ..^ 𝐾 ) )
271	270	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + 0 ) ∈ ( 0 ..^ 𝐾 ) )
272	75 77 264 271	ifbothda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) )
273	272	fmpttd	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
274		ovex	⊢ ( 0 ..^ 𝐾 ) ∈ V
275	274 48	elmap	⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
276	273 275	sylibr	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
277		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
278		1z	⊢ 1 ∈ ℤ
279	13 278	jctil	⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) )
280		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℤ )
281	280 278	jctir	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) )
282		fzaddel	⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
283	279 281 282	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
284	277 283	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
285	158	oveq2d	⊢ ( 𝜑 → ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 1 + 1 ) ... 𝑁 ) )
286	285	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 1 + 1 ) ... 𝑁 ) )
287	284 286	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... 𝑁 ) )
288	287	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... 𝑁 ) )
289		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
290		peano2z	⊢ ( 1 ∈ ℤ → ( 1 + 1 ) ∈ ℤ )
291	278 290	ax-mp	⊢ ( 1 + 1 ) ∈ ℤ
292	11 291	jctil	⊢ ( 𝜑 → ( ( 1 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
293		elfzelz	⊢ ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑦 ∈ ℤ )
294	293 278	jctir	⊢ ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) → ( 𝑦 ∈ ℤ ∧ 1 ∈ ℤ ) )
295		fzsubel	⊢ ( ( ( ( 1 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑦 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
296	292 294 295	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑦 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
297	289 296	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑦 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
298		ax-1cn	⊢ 1 ∈ ℂ
299	298 298	pncan3oi	⊢ ( ( 1 + 1 ) − 1 ) = 1
300	299	oveq1i	⊢ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
301	297 300	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑦 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
302	293	zcnd	⊢ ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑦 ∈ ℂ )
303		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℕ )
304	303	nncnd	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℂ )
305		subadd2	⊢ ( ( 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑛 ↔ ( 𝑛 + 1 ) = 𝑦 ) )
306	298 305	mp3an2	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑛 ↔ ( 𝑛 + 1 ) = 𝑦 ) )
307	306	bicomd	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑛 + 1 ) = 𝑦 ↔ ( 𝑦 − 1 ) = 𝑛 ) )
308		eqcom	⊢ ( 𝑦 = ( 𝑛 + 1 ) ↔ ( 𝑛 + 1 ) = 𝑦 )
309		eqcom	⊢ ( 𝑛 = ( 𝑦 − 1 ) ↔ ( 𝑦 − 1 ) = 𝑛 )
310	307 308 309	3bitr4g	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑦 = ( 𝑛 + 1 ) ↔ 𝑛 = ( 𝑦 − 1 ) ) )
311	302 304 310	syl2an	⊢ ( ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 = ( 𝑛 + 1 ) ↔ 𝑛 = ( 𝑦 − 1 ) ) )
312	311	ralrimiva	⊢ ( 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑦 = ( 𝑛 + 1 ) ↔ 𝑛 = ( 𝑦 − 1 ) ) )
313	312	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑦 = ( 𝑛 + 1 ) ↔ 𝑛 = ( 𝑦 − 1 ) ) )
314		reu6i	⊢ ( ( ( 𝑦 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ∀ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑦 = ( 𝑛 + 1 ) ↔ 𝑛 = ( 𝑦 − 1 ) ) ) → ∃! 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑦 = ( 𝑛 + 1 ) )
315	301 313 314	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ∃! 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑦 = ( 𝑛 + 1 ) )
316	315	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ∃! 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑦 = ( 𝑛 + 1 ) )
317		eqid	⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) = ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) )
318	317	f1ompt	⊢ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1-onto→ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( ∀ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑛 + 1 ) ∈ ( ( 1 + 1 ) ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( ( 1 + 1 ) ... 𝑁 ) ∃! 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑦 = ( 𝑛 + 1 ) ) )
319	288 316 318	sylanbrc	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1-onto→ ( ( 1 + 1 ) ... 𝑁 ) )
320		f1osng	⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ V ) → { ⟨ 𝑁 , 1 ⟩ } : { 𝑁 } –1-1-onto→ { 1 } )
321	1 130 320	sylancl	⊢ ( 𝜑 → { ⟨ 𝑁 , 1 ⟩ } : { 𝑁 } –1-1-onto→ { 1 } )
322	14 16	ltnled	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
323	20 322	mpbid	⊢ ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
324		elfzle2	⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
325	323 324	nsyl	⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
326		disjsn	⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
327	325 326	sylibr	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ )
328		1re	⊢ 1 ∈ ℝ
329	328	ltp1i	⊢ 1 < ( 1 + 1 )
330	291	zrei	⊢ ( 1 + 1 ) ∈ ℝ
331	328 330	ltnlei	⊢ ( 1 < ( 1 + 1 ) ↔ ¬ ( 1 + 1 ) ≤ 1 )
332	329 331	mpbi	⊢ ¬ ( 1 + 1 ) ≤ 1
333		elfzle1	⊢ ( 1 ∈ ( ( 1 + 1 ) ... 𝑁 ) → ( 1 + 1 ) ≤ 1 )
334	332 333	mto	⊢ ¬ 1 ∈ ( ( 1 + 1 ) ... 𝑁 )
335		disjsn	⊢ ( ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
336	334 335	mpbir	⊢ ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅
337	336	a1i	⊢ ( 𝜑 → ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅ )
338		f1oun	⊢ ( ( ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) : ( 1 ... ( 𝑁 − 1 ) ) –1-1-onto→ ( ( 1 + 1 ) ... 𝑁 ) ∧ { ⟨ 𝑁 , 1 ⟩ } : { 𝑁 } –1-1-onto→ { 1 } ) ∧ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ∧ ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅ ) ) → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) : ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) –1-1-onto→ ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) )
339	319 321 327 337 338	syl22anc	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) : ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) –1-1-onto→ ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) )
340	130	a1i	⊢ ( 𝜑 → 1 ∈ V )
341	158 97	eqeltrd	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
342		uzid	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
343		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
344	13 342 343	3syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
345	158 344	eqeltrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
346		fzsplit2	⊢ ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
347	341 345 346	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
348	158	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
349		fzsn	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
350	11 349	syl	⊢ ( 𝜑 → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
351	348 350	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } )
352	351	uneq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
353	347 352	eqtr2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) = ( 1 ... 𝑁 ) )
354		iftrue	⊢ ( 𝑛 = 𝑁 → if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) = 1 )
355	354	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) = 1 )
356	1 340 353 355	fmptapd	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) )
357		eleq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
358	357	notbid	⊢ ( 𝑛 = 𝑁 → ( ¬ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
359	325 358	syl5ibrcom	⊢ ( 𝜑 → ( 𝑛 = 𝑁 → ¬ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
360	359	necon2ad	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑛 ≠ 𝑁 ) )
361	360	imp	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑛 ≠ 𝑁 )
362		ifnefalse	⊢ ( 𝑛 ≠ 𝑁 → if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) = ( 𝑛 + 1 ) )
363	361 362	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) = ( 𝑛 + 1 ) )
364	363	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) = ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) )
365	364	uneq1d	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) = ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) )
366	356 365	eqtr3d	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) = ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) )
367	347 352	eqtrd	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
368		uzid	⊢ ( 1 ∈ ℤ → 1 ∈ ( ℤ_≥ ‘ 1 ) )
369		peano2uz	⊢ ( 1 ∈ ( ℤ_≥ ‘ 1 ) → ( 1 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
370	278 368 369	mp2b	⊢ ( 1 + 1 ) ∈ ( ℤ_≥ ‘ 1 )
371		fzsplit2	⊢ ( ( ( 1 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 1 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
372	370 97 371	sylancr	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
373		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
374	278 373	ax-mp	⊢ ( 1 ... 1 ) = { 1 }
375	374	uneq1i	⊢ ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... 𝑁 ) ) = ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) )
376	375	equncomi	⊢ ( ( 1 ... 1 ) ∪ ( ( 1 + 1 ) ... 𝑁 ) ) = ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } )
377	372 376	eqtrdi	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) )
378	366 367 377	f1oeq123d	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑛 + 1 ) ) ∪ { ⟨ 𝑁 , 1 ⟩ } ) : ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) –1-1-onto→ ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) ) )
379	339 378	mpbird	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
380		f1oco	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
381	93 379 380	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
382		f1oeq1	⊢ ( 𝑓 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
383	52 382	elab	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
384	381 383	sylibr	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
385	276 384	opelxpd	⊢ ( 𝜑 → ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
386	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
387		nn0fz0	⊢ ( 𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
388	386 387	sylib	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
389	385 388	opelxpd	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
390		elrab3t	⊢ ( ( ∀ 𝑡 ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) ) ∧ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ) → ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ { 𝑡 ∈ ( ( ( ( 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 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
391	73 389 390	syl2anc	⊢ ( 𝜑 → ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ { 𝑡 ∈ ( ( ( ( 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 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
392	7 391	mpbird	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ { 𝑡 ∈ ( ( ( ( 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 } ) ) ) ) } )
393	392 2	eleqtrrdi	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ 𝑆 )
394		fveqeq2	⊢ ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ = 𝑇 → ( ( 2^nd ‘ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ) = 𝑁 ↔ ( 2^nd ‘ 𝑇 ) = 𝑁 ) )
395	27 394	syl5ibcom	⊢ ( 𝜑 → ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ = 𝑇 → ( 2^nd ‘ 𝑇 ) = 𝑁 ) )
396	1	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
397		neeq1	⊢ ( ( 2^nd ‘ 𝑇 ) = 𝑁 → ( ( 2^nd ‘ 𝑇 ) ≠ 0 ↔ 𝑁 ≠ 0 ) )
398	396 397	syl5ibrcom	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) = 𝑁 → ( 2^nd ‘ 𝑇 ) ≠ 0 ) )
399	395 398	syld	⊢ ( 𝜑 → ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ = 𝑇 → ( 2^nd ‘ 𝑇 ) ≠ 0 ) )
400	399	necon2d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) = 0 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ≠ 𝑇 ) )
401	6 400	mpd	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ≠ 𝑇 )
402		neeq1	⊢ ( 𝑧 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ → ( 𝑧 ≠ 𝑇 ↔ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ≠ 𝑇 ) )
403	402	rspcev	⊢ ( ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ∈ 𝑆 ∧ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 1 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 𝑁 , 1 , ( 𝑛 + 1 ) ) ) ) ⟩ , 𝑁 ⟩ ≠ 𝑇 ) → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
404	393 401 403	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

Metamath Proof Explorer

Theorem poimirlem17

Proof