Metamath Proof Explorer

Theorem poimirlem22

Description: Lemma for poimir , that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (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 ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
poimirlem22.1 ⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
poimirlem22.2 ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
poimirlem22.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 )
poimirlem22.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
Assertion poimirlem22 ( 𝜑 → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimirlem22.s ⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
3 poimirlem22.1 ⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
4 poimirlem22.2 ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5 poimirlem22.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 )
6 poimirlem22.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
7 1 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑇 ∈ 𝑆 )
10 simpr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
11 7 2 8 9 10 poimirlem15 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ∈ 𝑆 )
12 fveq2 ⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑇 ) )
13 12 breq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑇 ) ) )
14 13 ifbid ⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
15 14 csbeq1d ⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
16 2fveq3 ⊢ ( 𝑡 = 𝑇 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
17 2fveq3 ⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) )
18 17 imaeq1d ⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
19 18 xpeq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
20 17 imaeq1d ⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
21 20 xpeq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
22 19 21 uneq12d ⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
23 16 22 oveq12d ⊢ ( 𝑡 = 𝑇 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
24 23 csbeq2dv ⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
25 15 24 eqtrd ⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
26 25 mpteq2dv ⊢ ( 𝑡 = 𝑇 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
27 26 eqeq2d ⊢ ( 𝑡 = 𝑇 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
28 27 2 elrab2 ⊢ ( 𝑇 ∈ 𝑆 ↔ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
29 28 simprbi ⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
30 4 29 syl ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
32 elrabi ⊢ ( 𝑇 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
33 32 2 eleq2s ⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
34 4 33 syl ⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
35 xp1st ⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
36 34 35 syl ⊢ ( 𝜑 → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
37 xp1st ⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
38 36 37 syl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
39 elmapi ⊢ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
40 38 39 syl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
41 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ 𝐾 ) → 𝑛 ∈ ℤ )
42 41 ssriv ⊢ ( 0 ..^ 𝐾 ) ⊆ ℤ
43 fss ⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
44 40 42 43 sylancl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
46 xp2nd ⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
47 36 46 syl ⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
48 fvex ⊢ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ V
49 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
50 48 49 elab ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
51 47 50 sylib ⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
53 7 31 45 52 10 poimirlem1 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) )
55 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → 𝑁 ∈ ℕ )
56 fveq2 ⊢ ( 𝑡 = 𝑧 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑧 ) )
57 56 breq2d ⊢ ( 𝑡 = 𝑧 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑧 ) ) )
58 57 ifbid ⊢ ( 𝑡 = 𝑧 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) )
59 58 csbeq1d ⊢ ( 𝑡 = 𝑧 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
60 2fveq3 ⊢ ( 𝑡 = 𝑧 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
61 2fveq3 ⊢ ( 𝑡 = 𝑧 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑧 ) ) )
62 61 imaeq1d ⊢ ( 𝑡 = 𝑧 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) )
63 62 xpeq1d ⊢ ( 𝑡 = 𝑧 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
64 61 imaeq1d ⊢ ( 𝑡 = 𝑧 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
65 64 xpeq1d ⊢ ( 𝑡 = 𝑧 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
66 63 65 uneq12d ⊢ ( 𝑡 = 𝑧 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
67 60 66 oveq12d ⊢ ( 𝑡 = 𝑧 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
68 67 csbeq2dv ⊢ ( 𝑡 = 𝑧 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
69 59 68 eqtrd ⊢ ( 𝑡 = 𝑧 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
70 69 mpteq2dv ⊢ ( 𝑡 = 𝑧 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
71 70 eqeq2d ⊢ ( 𝑡 = 𝑧 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
72 71 2 elrab2 ⊢ ( 𝑧 ∈ 𝑆 ↔ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
73 72 simprbi ⊢ ( 𝑧 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
74 73 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
75 elrabi ⊢ ( 𝑧 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
76 75 2 eleq2s ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
77 xp1st ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
78 76 77 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
79 xp1st ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
80 78 79 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
81 elmapi ⊢ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
82 80 81 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
83 fss ⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
84 82 42 83 sylancl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
85 84 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
86 xp2nd ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
87 78 86 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
88 fvex ⊢ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ V
89 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑧 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
90 88 89 elab ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
91 87 90 sylib ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
92 91 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
93 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
94 xp2nd ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) )
95 76 94 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) )
97 eldifsn ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) ↔ ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) )
98 97 biimpri ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) )
99 96 98 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) )
100 55 74 85 92 93 99 poimirlem2 ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) )
101 100 ex ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑧 ) ≠ ( 2nd ‘ 𝑇 ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) ) )
102 101 necon1bd ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) )
103 54 102 mpd ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) )
104 eleq1 ⊢ ( ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
105 104 biimparc ⊢ ( ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
106 105 anim2i ⊢ ( ( 𝜑 ∧ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) → ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
107 106 anassrs ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
108 73 adantl ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
109 breq1 ⊢ ( 𝑦 = 0 → ( 𝑦 < ( 2nd ‘ 𝑧 ) ↔ 0 < ( 2nd ‘ 𝑧 ) ) )
110 id ⊢ ( 𝑦 = 0 → 𝑦 = 0 )
111 109 110 ifbieq1d ⊢ ( 𝑦 = 0 → if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 0 < ( 2nd ‘ 𝑧 ) , 0 , ( 𝑦 + 1 ) ) )
112 elfznn ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑧 ) ∈ ℕ )
113 112 nngt0d ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → 0 < ( 2nd ‘ 𝑧 ) )
114 113 iftrued ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → if ( 0 < ( 2nd ‘ 𝑧 ) , 0 , ( 𝑦 + 1 ) ) = 0 )
115 114 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → if ( 0 < ( 2nd ‘ 𝑧 ) , 0 , ( 𝑦 + 1 ) ) = 0 )
116 111 115 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑦 = 0 ) → if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) = 0 )
117 116 csbeq1d ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑦 = 0 ) → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 0 / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
118 c0ex ⊢ 0 ∈ V
119 oveq2 ⊢ ( 𝑗 = 0 → ( 1 ... 𝑗 ) = ( 1 ... 0 ) )
120 fz10 ⊢ ( 1 ... 0 ) = ∅
121 119 120 eqtrdi ⊢ ( 𝑗 = 0 → ( 1 ... 𝑗 ) = ∅ )
122 121 imaeq2d ⊢ ( 𝑗 = 0 → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) )
123 122 xpeq1d ⊢ ( 𝑗 = 0 → ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) )
124 oveq1 ⊢ ( 𝑗 = 0 → ( 𝑗 + 1 ) = ( 0 + 1 ) )
125 0p1e1 ⊢ ( 0 + 1 ) = 1
126 124 125 eqtrdi ⊢ ( 𝑗 = 0 → ( 𝑗 + 1 ) = 1 )
127 126 oveq1d ⊢ ( 𝑗 = 0 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 ) )
128 127 imaeq2d ⊢ ( 𝑗 = 0 → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) )
129 128 xpeq1d ⊢ ( 𝑗 = 0 → ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) )
130 123 129 uneq12d ⊢ ( 𝑗 = 0 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) )
131 ima0 ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) = ∅
132 131 xpeq1i ⊢ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) = ( ∅ × { 1 } )
133 0xp ⊢ ( ∅ × { 1 } ) = ∅
134 132 133 eqtri ⊢ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) = ∅
135 134 uneq1i ⊢ ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) = ( ∅ ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) )
136 uncom ⊢ ( ∅ ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ∪ ∅ )
137 un0 ⊢ ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ∪ ∅ ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } )
138 135 136 137 3eqtri ⊢ ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ∅ ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } )
139 130 138 eqtrdi ⊢ ( 𝑗 = 0 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) )
140 139 oveq2d ⊢ ( 𝑗 = 0 → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) )
141 118 140 csbie ⊢ ⦋ 0 / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) )
142 f1ofo ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
143 91 142 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
144 foima ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
145 143 144 syl ⊢ ( 𝑧 ∈ 𝑆 → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
146 145 xpeq1d ⊢ ( 𝑧 ∈ 𝑆 → ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) = ( ( 1 ... 𝑁 ) × { 0 } ) )
147 146 oveq2d ⊢ ( 𝑧 ∈ 𝑆 → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( 1 ... 𝑁 ) × { 0 } ) ) )
148 ovexd ⊢ ( 𝑧 ∈ 𝑆 → ( 1 ... 𝑁 ) ∈ V )
149 82 ffnd ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) Fn ( 1 ... 𝑁 ) )
150 fnconstg ⊢ ( 0 ∈ V → ( ( 1 ... 𝑁 ) × { 0 } ) Fn ( 1 ... 𝑁 ) )
151 118 150 mp1i ⊢ ( 𝑧 ∈ 𝑆 → ( ( 1 ... 𝑁 ) × { 0 } ) Fn ( 1 ... 𝑁 ) )
152 eqidd ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) )
153 118 fvconst2 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) = 0 )
154 153 adantl ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) = 0 )
155 82 ffvelrnda ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) )
156 elfzonn0 ⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ ℕ0 )
157 155 156 syl ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ ℕ0 )
158 157 nn0cnd ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ ℂ )
159 158 addid1d ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) + 0 ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ‘ 𝑛 ) )
160 148 149 151 149 152 154 159 offveq ⊢ ( 𝑧 ∈ 𝑆 → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( 1 ... 𝑁 ) × { 0 } ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
161 147 160 eqtrd ⊢ ( 𝑧 ∈ 𝑆 → ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑁 ) ) × { 0 } ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
162 141 161 syl5eq ⊢ ( 𝑧 ∈ 𝑆 → ⦋ 0 / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
163 162 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑦 = 0 ) → ⦋ 0 / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
164 117 163 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑦 = 0 ) → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
165 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
166 1 165 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
167 0elfz ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
168 166 167 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
169 168 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 0 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
170 fvexd ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ V )
171 108 164 169 170 fvmptd ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
172 107 171 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
173 172 an32s ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
174 103 173 mpdan ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
175 fveq2 ⊢ ( 𝑧 = 𝑇 → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) )
176 175 eleq1d ⊢ ( 𝑧 = 𝑇 → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
177 176 anbi2d ⊢ ( 𝑧 = 𝑇 → ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) )
178 2fveq3 ⊢ ( 𝑧 = 𝑇 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
179 178 eqeq2d ⊢ ( 𝑧 = 𝑇 → ( ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) ↔ ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ) )
180 177 179 imbi12d ⊢ ( 𝑧 = 𝑇 → ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) ) ↔ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ) ) )
181 171 expcom ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) ) )
182 180 181 vtoclga ⊢ ( 𝑇 ∈ 𝑆 → ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ) )
183 9 182 mpcom ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
184 183 adantr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
185 174 184 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
186 185 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
187 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → 𝑁 ∈ ℕ )
188 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → 𝑇 ∈ 𝑆 )
189 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
190 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → 𝑧 ∈ 𝑆 )
191 36 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
192 xpopth ⊢ ( ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ) → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ) ↔ ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) ) )
193 78 191 192 syl2anr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ) ↔ ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) ) )
194 34 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
195 xpopth ⊢ ( ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ) → ( ( ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ↔ 𝑧 = 𝑇 ) )
196 195 biimpd ⊢ ( ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ) → ( ( ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → 𝑧 = 𝑇 ) )
197 76 194 196 syl2anr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → 𝑧 = 𝑇 ) )
198 103 197 mpan2d ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑇 ) → 𝑧 = 𝑇 ) )
199 193 198 sylbid ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ) → 𝑧 = 𝑇 ) )
200 185 199 mpand ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) → 𝑧 = 𝑇 ) )
201 200 necon3d ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ≠ 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ≠ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ) )
202 201 imp ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ≠ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) )
203 187 2 188 189 190 202 poimirlem9 ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )
204 103 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) )
205 186 203 204 jca31 ⊢ ( ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 ≠ 𝑇 ) → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) )
206 205 ex ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ≠ 𝑇 → ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
207 simplr ⊢ ( ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )
208 elfznn ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) ∈ ℕ )
209 208 nnred ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) ∈ ℝ )
210 209 ltp1d ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) < ( ( 2nd ‘ 𝑇 ) + 1 ) )
211 209 210 ltned ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) )
212 211 adantl ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) )
213 fveq1 ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) )
214 id ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( 2nd ‘ 𝑇 ) ∈ ℝ )
215 ltp1 ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( 2nd ‘ 𝑇 ) < ( ( 2nd ‘ 𝑇 ) + 1 ) )
216 214 215 ltned ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) )
217 fvex ⊢ ( 2nd ‘ 𝑇 ) ∈ V
218 ovex ⊢ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ V
219 217 218 218 217 fpr ⊢ ( ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) → { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } : { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } )
220 216 219 syl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } : { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } )
221 f1oi ⊢ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
222 f1of ⊢ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) → ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⟶ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
223 221 222 ax-mp ⊢ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⟶ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
224 disjdif ⊢ ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ∅
225 fun ⊢ ( ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } : { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∧ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⟶ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ∧ ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ∅ ) → ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ⟶ ( { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )
226 224 225 mpan2 ⊢ ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } : { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ⟶ { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∧ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⟶ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ⟶ ( { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )
227 220 223 226 sylancl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ⟶ ( { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )
228 217 prid1 ⊢ ( 2nd ‘ 𝑇 ) ∈ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) }
229 elun1 ⊢ ( ( 2nd ‘ 𝑇 ) ∈ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } → ( 2nd ‘ 𝑇 ) ∈ ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )
230 228 229 ax-mp ⊢ ( 2nd ‘ 𝑇 ) ∈ ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
231 fvco3 ⊢ ( ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ⟶ ( { ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ∧ ( 2nd ‘ 𝑇 ) ∈ ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) ) )
232 227 230 231 sylancl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) ) )
233 220 ffnd ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } Fn { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
234 fnresi ⊢ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
235 224 228 pm3.2i ⊢ ( ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ∅ ∧ ( 2nd ‘ 𝑇 ) ∈ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
236 fvun1 ⊢ ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } Fn { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∧ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∧ ( ( { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ∅ ∧ ( 2nd ‘ 𝑇 ) ∈ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ‘ ( 2nd ‘ 𝑇 ) ) )
237 234 235 236 mp3an23 ⊢ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } Fn { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } → ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ‘ ( 2nd ‘ 𝑇 ) ) )
238 233 237 syl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ‘ ( 2nd ‘ 𝑇 ) ) )
239 217 218 fvpr1 ⊢ ( ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) → ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ 𝑇 ) + 1 ) )
240 216 239 syl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ 𝑇 ) + 1 ) )
241 238 240 eqtrd ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ 𝑇 ) + 1 ) )
242 241 fveq2d ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
243 232 242 eqtrd ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
244 209 243 syl ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
245 244 eqeq2d ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) ↔ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) ) )
246 245 adantl ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) ↔ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) ) )
247 f1of1 ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
248 51 247 syl ⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
249 248 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
250 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
251 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
252 250 251 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
253 166 nn0zd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
254 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
255 253 254 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
256 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
257 255 256 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
258 252 257 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
259 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
260 258 259 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
261 260 sselda ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) )
262 fzp1elp1 ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
263 262 adantl ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
264 252 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
265 264 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
266 263 265 eleqtrd ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) )
267 f1veqaeq ⊢ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... 𝑁 ) ∧ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) → ( 2nd ‘ 𝑇 ) = ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
268 249 261 266 267 syl12anc ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( ( 2nd ‘ 𝑇 ) + 1 ) ) → ( 2nd ‘ 𝑇 ) = ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
269 246 268 sylbid ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ ( 2nd ‘ 𝑇 ) ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ‘ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑇 ) = ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
270 213 269 syl5 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) → ( 2nd ‘ 𝑇 ) = ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
271 270 necon3d ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) ≠ ( ( 2nd ‘ 𝑇 ) + 1 ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ≠ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) )
272 212 271 mpd ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ≠ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) )
273 2fveq3 ⊢ ( 𝑧 = 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) )
274 273 neeq1d ⊢ ( 𝑧 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ≠ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ≠ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) )
275 272 274 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑧 = 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ≠ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) )
276 275 necon2d ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) → 𝑧 ≠ 𝑇 ) )
277 207 276 syl5 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → 𝑧 ≠ 𝑇 ) )
278 277 adantr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) → 𝑧 ≠ 𝑇 ) )
279 206 278 impbid ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ≠ 𝑇 ↔ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
280 eqop ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ↔ ( ( 1st ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
281 eqop ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( ( 1st ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ ↔ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ) )
282 77 281 syl ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( ( 1st ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ ↔ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ) )
283 282 anbi1d ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( ( ( 1st ‘ 𝑧 ) = ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ↔ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
284 280 283 bitrd ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ↔ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
285 76 284 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ↔ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
286 285 adantl ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ↔ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∧ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ) ∧ ( 2nd ‘ 𝑧 ) = ( 2nd ‘ 𝑇 ) ) ) )
287 279 286 bitr4d ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ) )
288 287 ralrimiva ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ) )
289 reu6i ⊢ ( ( ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑇 ) ) , ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∘ ( { ⟨ ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd ‘ 𝑇 ) + 1 ) , ( 2nd ‘ 𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd ‘ 𝑇 ) ⟩ ) ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
290 11 288 289 syl2anc ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
291 xp2nd ⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) )
292 34 291 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) )
293 292 biantrurd ⊢ ( 𝜑 → ( ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) )
294 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
295 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
296 294 295 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
297 fzpred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) )
298 296 297 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) )
299 125 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 )
300 299 uneq2i ⊢ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) = ( { 0 } ∪ ( 1 ... 𝑁 ) )
301 298 300 eqtrdi ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
302 301 difeq1d ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( ( { 0 } ∪ ( 1 ... 𝑁 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
303 difundir ⊢ ( ( { 0 } ∪ ( 1 ... 𝑁 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( ( { 0 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
304 0lt1 ⊢ 0 < 1
305 0re ⊢ 0 ∈ ℝ
306 1re ⊢ 1 ∈ ℝ
307 305 306 ltnlei ⊢ ( 0 < 1 ↔ ¬ 1 ≤ 0 )
308 304 307 mpbi ⊢ ¬ 1 ≤ 0
309 elfzle1 ⊢ ( 0 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 1 ≤ 0 )
310 308 309 mto ⊢ ¬ 0 ∈ ( 1 ... ( 𝑁 − 1 ) )
311 incom ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 0 } ) = ( { 0 } ∩ ( 1 ... ( 𝑁 − 1 ) ) )
312 311 eqeq1i ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 0 } ) = ∅ ↔ ( { 0 } ∩ ( 1 ... ( 𝑁 − 1 ) ) ) = ∅ )
313 disjsn ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
314 disj3 ⊢ ( ( { 0 } ∩ ( 1 ... ( 𝑁 − 1 ) ) ) = ∅ ↔ { 0 } = ( { 0 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
315 312 313 314 3bitr3i ⊢ ( ¬ 0 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ { 0 } = ( { 0 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
316 310 315 mpbi ⊢ { 0 } = ( { 0 } ∖ ( 1 ... ( 𝑁 − 1 ) ) )
317 316 uneq1i ⊢ ( { 0 } ∪ ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( ( { 0 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
318 303 317 eqtr4i ⊢ ( ( { 0 } ∪ ( 1 ... 𝑁 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( { 0 } ∪ ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
319 difundir ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( ( ( 1 ... ( 𝑁 − 1 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
320 difid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ∅
321 320 uneq1i ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( ∅ ∪ ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
322 uncom ⊢ ( ∅ ∪ ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ∅ )
323 un0 ⊢ ( ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ∪ ∅ ) = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) )
324 322 323 eqtri ⊢ ( ∅ ∪ ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) )
325 319 321 324 3eqtri ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) )
326 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
327 1 326 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
328 252 327 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
329 fzsplit2 ⊢ ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
330 328 258 329 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
331 252 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
332 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
333 fzsn ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
334 332 333 syl ⊢ ( 𝜑 → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
335 331 334 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } )
336 335 uneq2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
337 330 336 eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
338 337 difeq1d ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
339 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
340 339 ltm1d ⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
341 166 nn0red ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
342 341 339 ltnled ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
343 340 342 mpbid ⊢ ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
344 elfzle2 ⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
345 343 344 nsyl ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
346 incom ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ( { 𝑁 } ∩ ( 1 ... ( 𝑁 − 1 ) ) )
347 346 eqeq1i ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ( { 𝑁 } ∩ ( 1 ... ( 𝑁 − 1 ) ) ) = ∅ )
348 disjsn ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
349 disj3 ⊢ ( ( { 𝑁 } ∩ ( 1 ... ( 𝑁 − 1 ) ) ) = ∅ ↔ { 𝑁 } = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
350 347 348 349 3bitr3i ⊢ ( ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ { 𝑁 } = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
351 345 350 sylib ⊢ ( 𝜑 → { 𝑁 } = ( { 𝑁 } ∖ ( 1 ... ( 𝑁 − 1 ) ) ) )
352 325 338 351 3eqtr4a ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = { 𝑁 } )
353 352 uneq2d ⊢ ( 𝜑 → ( { 0 } ∪ ( ( 1 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( { 0 } ∪ { 𝑁 } ) )
354 318 353 syl5eq ⊢ ( 𝜑 → ( ( { 0 } ∪ ( 1 ... 𝑁 ) ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( { 0 } ∪ { 𝑁 } ) )
355 302 354 eqtrd ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) = ( { 0 } ∪ { 𝑁 } ) )
356 355 eleq2d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( 2nd ‘ 𝑇 ) ∈ ( { 0 } ∪ { 𝑁 } ) ) )
357 eldif ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
358 elun ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( { 0 } ∪ { 𝑁 } ) ↔ ( ( 2nd ‘ 𝑇 ) ∈ { 0 } ∨ ( 2nd ‘ 𝑇 ) ∈ { 𝑁 } ) )
359 217 elsn ⊢ ( ( 2nd ‘ 𝑇 ) ∈ { 0 } ↔ ( 2nd ‘ 𝑇 ) = 0 )
360 217 elsn ⊢ ( ( 2nd ‘ 𝑇 ) ∈ { 𝑁 } ↔ ( 2nd ‘ 𝑇 ) = 𝑁 )
361 359 360 orbi12i ⊢ ( ( ( 2nd ‘ 𝑇 ) ∈ { 0 } ∨ ( 2nd ‘ 𝑇 ) ∈ { 𝑁 } ) ↔ ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) )
362 358 361 bitri ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( { 0 } ∪ { 𝑁 } ) ↔ ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) )
363 356 357 362 3bitr3g ⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) ) )
364 293 363 bitrd ⊢ ( 𝜑 → ( ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) ) )
365 364 biimpa ⊢ ( ( 𝜑 ∧ ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) )
366 1 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) → 𝑁 ∈ ℕ )
367 3 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
368 4 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) → 𝑇 ∈ 𝑆 )
369 6 adantlr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
370 simpr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) → ( 2nd ‘ 𝑇 ) = 0 )
371 366 2 367 368 369 370 poimirlem18 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 0 ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
372 1 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝑁 ∈ ℕ )
373 3 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
374 4 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝑇 ∈ 𝑆 )
375 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 )
376 simpr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → ( 2nd ‘ 𝑇 ) = 𝑁 )
377 372 2 373 374 375 376 poimirlem21 ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
378 371 377 jaodan ⊢ ( ( 𝜑 ∧ ( ( 2nd ‘ 𝑇 ) = 0 ∨ ( 2nd ‘ 𝑇 ) = 𝑁 ) ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
379 365 378 syldan ⊢ ( ( 𝜑 ∧ ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
380 290 379 pm2.61dan ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )