Metamath Proof Explorer

Theorem poimirlem18

Description: Lemma for poimir stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on 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 ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
poimirlem18.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 𝐾 )
poimirlem18.4 ⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) = 0 )
Assertion poimirlem18 ( 𝜑 → ∃! 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

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