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