Metamath Proof Explorer

Theorem poimirlem21

Description: Lemma for poimir stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (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 )
poimirlem21.4 ⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) = 𝑁 )
Assertion poimirlem21 ( 𝜑 → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

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 poimirlem21.4 ⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) = 𝑁 )
7 1 2 3 4 5 6 poimirlem20 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
8 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 2nd ‘ 𝑇 ) = 𝑁 )
9 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 9 ltm1d ⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
11 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
12 1 11 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
13 12 nn0red ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
14 13 9 ltnled ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
15 10 14 mpbid ⊢ ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
16 elfzle2 ⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
17 15 16 nsyl ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
18 eleq1 ⊢ ( ( 2nd ‘ 𝑧 ) = 𝑁 → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
19 18 notbid ⊢ ( ( 2nd ‘ 𝑧 ) = 𝑁 → ( ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
20 17 19 syl5ibrcom ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑧 ) = 𝑁 → ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
21 20 necon2ad ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑧 ) ≠ 𝑁 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑧 ) ≠ 𝑁 ) )
23 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
24 fveq2 ⊢ ( 𝑡 = 𝑧 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑧 ) )
25 24 breq2d ⊢ ( 𝑡 = 𝑧 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑧 ) ) )
26 25 ifbid ⊢ ( 𝑡 = 𝑧 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) )
27 26 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 } ) ) ) )
28 2fveq3 ⊢ ( 𝑡 = 𝑧 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑧 ) ) )
29 2fveq3 ⊢ ( 𝑡 = 𝑧 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑧 ) ) )
30 29 imaeq1d ⊢ ( 𝑡 = 𝑧 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) )
31 30 xpeq1d ⊢ ( 𝑡 = 𝑧 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
32 29 imaeq1d ⊢ ( 𝑡 = 𝑧 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
33 32 xpeq1d ⊢ ( 𝑡 = 𝑧 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
34 31 33 uneq12d ⊢ ( 𝑡 = 𝑧 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
35 28 34 oveq12d ⊢ ( 𝑡 = 𝑧 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
36 35 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 } ) ) ) )
37 27 36 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 } ) ) ) )
38 37 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 } ) ) ) ) )
39 38 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 } ) ) ) ) ) )
40 39 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 } ) ) ) ) ) )
41 40 simprbi ⊢ ( 𝑧 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
42 41 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑧 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
43 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 ... 𝑁 ) ) )
44 43 2 eleq2s ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
45 xp1st ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
46 44 45 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
47 xp1st ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
48 46 47 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
49 elmapi ⊢ ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
50 48 49 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
51 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ 𝐾 ) → 𝑛 ∈ ℤ )
52 51 ssriv ⊢ ( 0 ..^ 𝐾 ) ⊆ ℤ
53 fss ⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
54 50 52 53 sylancl ⊢ ( 𝑧 ∈ 𝑆 → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
55 54 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1st ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
56 xp2nd ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
57 46 56 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
58 fvex ⊢ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ V
59 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑧 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
60 58 59 elab ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑧 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
61 57 60 sylib ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
62 61 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ ( 1st ‘ 𝑧 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
63 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
64 23 42 55 62 63 poimirlem1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑧 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ‘ 𝑛 ) )
65 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → 𝑁 ∈ ℕ )
66 fveq2 ⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑇 ) )
67 66 breq2d ⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑇 ) ) )
68 67 ifbid ⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
69 68 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 } ) ) ) )
70 2fveq3 ⊢ ( 𝑡 = 𝑇 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
71 2fveq3 ⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) )
72 71 imaeq1d ⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
73 72 xpeq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
74 71 imaeq1d ⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
75 74 xpeq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
76 73 75 uneq12d ⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
77 70 76 oveq12d ⊢ ( 𝑡 = 𝑇 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
78 77 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 } ) ) ) )
79 69 78 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 } ) ) ) )
80 79 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 } ) ) ) ) )
81 80 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 } ) ) ) ) ) )
82 81 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 } ) ) ) ) ) )
83 82 simprbi ⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
84 4 83 syl ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
85 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
86 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 ... 𝑁 ) ) )
87 86 2 eleq2s ⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
88 4 87 syl ⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
89 xp1st ⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
90 88 89 syl ⊢ ( 𝜑 → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
91 xp1st ⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
92 90 91 syl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
93 elmapi ⊢ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
94 92 93 syl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
95 fss ⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
96 94 52 95 sylancl ⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
97 96 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
98 xp2nd ⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
99 90 98 syl ⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
100 fvex ⊢ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ V
101 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
102 100 101 elab ⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
103 99 102 sylib ⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
105 simplr ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
106 xp2nd ⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) )
107 88 106 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) )
108 107 adantr ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) )
109 eldifsn ⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑧 ) } ) ↔ ( ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) )
110 109 biimpri ⊢ ( ( ( 2nd ‘ 𝑇 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑧 ) } ) )
111 108 110 sylan ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑧 ) } ) )
112 65 85 97 104 105 111 poimirlem2 ⊢ ( ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑧 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ‘ 𝑛 ) )
113 112 ex ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) ≠ ( 2nd ‘ 𝑧 ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑧 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ‘ 𝑛 ) ) )
114 113 necon1bd ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑧 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ‘ 𝑛 ) → ( 2nd ‘ 𝑇 ) = ( 2nd ‘ 𝑧 ) ) )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑧 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ‘ 𝑛 ) → ( 2nd ‘ 𝑇 ) = ( 2nd ‘ 𝑧 ) ) )
116 64 115 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑇 ) = ( 2nd ‘ 𝑧 ) )
117 116 neeq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd ‘ 𝑇 ) ≠ 𝑁 ↔ ( 2nd ‘ 𝑧 ) ≠ 𝑁 ) )
118 117 exbiri ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 2nd ‘ 𝑧 ) ≠ 𝑁 → ( 2nd ‘ 𝑇 ) ≠ 𝑁 ) ) )
119 22 118 mpdd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) ≠ 𝑁 ) )
120 119 necon2bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑇 ) = 𝑁 → ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
121 8 120 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
122 xp2nd ⊢ ( 𝑧 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) )
123 44 122 syl ⊢ ( 𝑧 ∈ 𝑆 → ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) )
124 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
125 12 124 eleqtrdi ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
126 fzpred ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... ( 𝑁 − 1 ) ) = ( { 0 } ∪ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) )
127 125 126 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) = ( { 0 } ∪ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) )
128 0p1e1 ⊢ ( 0 + 1 ) = 1
129 128 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
130 129 uneq2i ⊢ ( { 0 } ∪ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) = ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) )
131 127 130 eqtrdi ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) = ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) )
132 131 eleq2d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 2nd ‘ 𝑧 ) ∈ ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) ) )
133 132 notbid ⊢ ( 𝜑 → ( ¬ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ¬ ( 2nd ‘ 𝑧 ) ∈ ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) ) )
134 ioran ⊢ ( ¬ ( ( 2nd ‘ 𝑧 ) = 0 ∨ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
135 elun ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑧 ) ∈ { 0 } ∨ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
136 fvex ⊢ ( 2nd ‘ 𝑧 ) ∈ V
137 136 elsn ⊢ ( ( 2nd ‘ 𝑧 ) ∈ { 0 } ↔ ( 2nd ‘ 𝑧 ) = 0 )
138 137 orbi1i ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ { 0 } ∨ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑧 ) = 0 ∨ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
139 135 138 bitri ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑧 ) = 0 ∨ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
140 134 139 xchnxbir ⊢ ( ¬ ( 2nd ‘ 𝑧 ) ∈ ( { 0 } ∪ ( 1 ... ( 𝑁 − 1 ) ) ) ↔ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) )
141 133 140 bitrdi ⊢ ( 𝜑 → ( ¬ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) )
142 141 anbi2d ⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )
143 uncom ⊢ ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) = ( { 𝑁 } ∪ ( 0 ... ( 𝑁 − 1 ) ) )
144 143 difeq1i ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ( { 𝑁 } ∪ ( 0 ... ( 𝑁 − 1 ) ) ) ∖ ( 0 ... ( 𝑁 − 1 ) ) )
145 difun2 ⊢ ( ( { 𝑁 } ∪ ( 0 ... ( 𝑁 − 1 ) ) ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) = ( { 𝑁 } ∖ ( 0 ... ( 𝑁 − 1 ) ) )
146 144 145 eqtri ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) = ( { 𝑁 } ∖ ( 0 ... ( 𝑁 − 1 ) ) )
147 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
148 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
149 147 148 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
150 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
151 150 124 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
152 149 151 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
153 12 nn0zd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
154 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
155 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
156 153 154 155 3syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
157 149 156 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
158 fzsplit2 ⊢ ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ) → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
159 152 157 158 syl2anc ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
160 149 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
161 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
162 fzsn ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
163 161 162 syl ⊢ ( 𝜑 → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
164 160 163 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } )
165 164 uneq2d ⊢ ( 𝜑 → ( ( 0 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
166 159 165 eqtrd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
167 166 difeq1d ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ( ( 0 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) )
168 elfzle2 ⊢ ( 𝑁 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
169 15 168 nsyl ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
170 incom ⊢ ( ( 0 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ( { 𝑁 } ∩ ( 0 ... ( 𝑁 − 1 ) ) )
171 170 eqeq1i ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ( { 𝑁 } ∩ ( 0 ... ( 𝑁 − 1 ) ) ) = ∅ )
172 disjsn ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
173 disj3 ⊢ ( ( { 𝑁 } ∩ ( 0 ... ( 𝑁 − 1 ) ) ) = ∅ ↔ { 𝑁 } = ( { 𝑁 } ∖ ( 0 ... ( 𝑁 − 1 ) ) ) )
174 171 172 173 3bitr3i ⊢ ( ¬ 𝑁 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ { 𝑁 } = ( { 𝑁 } ∖ ( 0 ... ( 𝑁 − 1 ) ) ) )
175 169 174 sylib ⊢ ( 𝜑 → { 𝑁 } = ( { 𝑁 } ∖ ( 0 ... ( 𝑁 − 1 ) ) ) )
176 146 167 175 3eqtr4a ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) = { 𝑁 } )
177 176 eleq2d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑧 ) ∈ ( ( 0 ... 𝑁 ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( 2nd ‘ 𝑧 ) ∈ { 𝑁 } ) )
178 eldif ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( ( 0 ... 𝑁 ) ∖ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
179 136 elsn ⊢ ( ( 2nd ‘ 𝑧 ) ∈ { 𝑁 } ↔ ( 2nd ‘ 𝑧 ) = 𝑁 )
180 177 178 179 3bitr3g ⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( 2nd ‘ 𝑧 ) = 𝑁 ) )
181 142 180 bitr3d ⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) ↔ ( 2nd ‘ 𝑧 ) = 𝑁 ) )
182 181 biimpd ⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ∧ ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 2nd ‘ 𝑧 ) = 𝑁 ) )
183 182 expdimp ⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 0 ... 𝑁 ) ) → ( ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑧 ) = 𝑁 ) )
184 123 183 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( ¬ ( 2nd ‘ 𝑧 ) = 0 ∧ ¬ ( 2nd ‘ 𝑧 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 2nd ‘ 𝑧 ) = 𝑁 ) )
185 121 184 mpan2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ¬ ( 2nd ‘ 𝑧 ) = 0 → ( 2nd ‘ 𝑧 ) = 𝑁 ) )
186 1 2 3 poimirlem14 ⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 ( 2nd ‘ 𝑧 ) = 𝑁 )
187 fveqeq2 ⊢ ( 𝑧 = 𝑠 → ( ( 2nd ‘ 𝑧 ) = 𝑁 ↔ ( 2nd ‘ 𝑠 ) = 𝑁 ) )
188 187 rmo4 ⊢ ( ∃* 𝑧 ∈ 𝑆 ( 2nd ‘ 𝑧 ) = 𝑁 ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑠 ∈ 𝑆 ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) → 𝑧 = 𝑠 ) )
189 186 188 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ∀ 𝑠 ∈ 𝑆 ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) → 𝑧 = 𝑠 ) )
190 189 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ∀ 𝑠 ∈ 𝑆 ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) → 𝑧 = 𝑠 ) )
191 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑇 ∈ 𝑆 )
192 fveqeq2 ⊢ ( 𝑠 = 𝑇 → ( ( 2nd ‘ 𝑠 ) = 𝑁 ↔ ( 2nd ‘ 𝑇 ) = 𝑁 ) )
193 192 anbi2d ⊢ ( 𝑠 = 𝑇 → ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) ↔ ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) ) )
194 eqeq2 ⊢ ( 𝑠 = 𝑇 → ( 𝑧 = 𝑠 ↔ 𝑧 = 𝑇 ) )
195 193 194 imbi12d ⊢ ( 𝑠 = 𝑇 → ( ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) → 𝑧 = 𝑠 ) ↔ ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝑧 = 𝑇 ) ) )
196 195 rspccv ⊢ ( ∀ 𝑠 ∈ 𝑆 ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑠 ) = 𝑁 ) → 𝑧 = 𝑠 ) → ( 𝑇 ∈ 𝑆 → ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝑧 = 𝑇 ) ) )
197 190 191 196 sylc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 2nd ‘ 𝑧 ) = 𝑁 ∧ ( 2nd ‘ 𝑇 ) = 𝑁 ) → 𝑧 = 𝑇 ) )
198 8 197 mpan2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 2nd ‘ 𝑧 ) = 𝑁 → 𝑧 = 𝑇 ) )
199 185 198 syld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ¬ ( 2nd ‘ 𝑧 ) = 0 → 𝑧 = 𝑇 ) )
200 199 necon1ad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑧 ≠ 𝑇 → ( 2nd ‘ 𝑧 ) = 0 ) )
201 200 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝑇 → ( 2nd ‘ 𝑧 ) = 0 ) )
202 1 2 3 poimirlem13 ⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 ( 2nd ‘ 𝑧 ) = 0 )
203 rmoim ⊢ ( ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝑇 → ( 2nd ‘ 𝑧 ) = 0 ) → ( ∃* 𝑧 ∈ 𝑆 ( 2nd ‘ 𝑧 ) = 0 → ∃* 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ) )
204 201 202 203 sylc ⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
205 reu5 ⊢ ( ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ↔ ( ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃* 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ) )
206 7 204 205 sylanbrc ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )