Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem22 Structured version   Visualization version   GIF version

Theorem poimirlem22 32601
 Description: Lemma for poimir 32612, 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.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
poimirlem22.2 (𝜑𝑇𝑆)
poimirlem22.3 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)
poimirlem22.4 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
Assertion
Ref Expression
poimirlem22 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
Distinct variable groups:   𝑓,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑝,𝑡   𝑓,𝐾,𝑗,𝑛,𝑝,𝑡   𝑓,𝑁,𝑝,𝑡   𝑇,𝑓,𝑝   𝜑,𝑧   𝑓,𝐹,𝑝,𝑡,𝑧   𝑧,𝐾   𝑧,𝑁   𝑡,𝑇,𝑧   𝑆,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem22
StepHypRef Expression
1 poimir.0 . . . . 5 (𝜑𝑁 ∈ ℕ)
21adantr 480 . . . 4 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
3 poimirlem22.s . . . 4 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4 poimirlem22.1 . . . . 5 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
54adantr 480 . . . 4 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
6 poimirlem22.2 . . . . 5 (𝜑𝑇𝑆)
76adantr 480 . . . 4 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → 𝑇𝑆)
8 simpr 476 . . . 4 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ∈ (1...(𝑁 − 1)))
92, 3, 5, 7, 8poimirlem15 32594 . . 3 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ 𝑆)
10 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
1110breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
1211ifbid 4058 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
1312csbeq1d 3506 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
14 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
1514fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
1614fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
1716imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
1817xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
1916imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
2019xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
2118, 20uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
2215, 21oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
2322csbeq2dv 3944 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
2413, 23eqtrd 2644 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
2524mpteq2dv 4673 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
2625eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
2726, 3elrab2 3333 . . . . . . . . . . . . . . . . 17 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
2827simprbi 479 . . . . . . . . . . . . . . . 16 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
296, 28syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
3029adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
31 elrabi 3328 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3231, 3eleq2s 2706 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
336, 32syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
34 xp1st 7089 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3533, 34syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
36 xp1st 7089 . . . . . . . . . . . . . . . . . 18 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
3735, 36syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
38 elmapi 7765 . . . . . . . . . . . . . . . . 17 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
3937, 38syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
40 elfzoelz 12339 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
4140ssriv 3572 . . . . . . . . . . . . . . . 16 (0..^𝐾) ⊆ ℤ
42 fss 5969 . . . . . . . . . . . . . . . 16 (((1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
4339, 41, 42sylancl 693 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
4443adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
45 xp2nd 7090 . . . . . . . . . . . . . . . . 17 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
4635, 45syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
47 fvex 6113 . . . . . . . . . . . . . . . . 17 (2nd ‘(1st𝑇)) ∈ V
48 f1oeq1 6040 . . . . . . . . . . . . . . . . 17 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4947, 48elab 3319 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
5046, 49sylib 207 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
5150adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
522, 30, 44, 51, 8poimirlem1 32580 . . . . . . . . . . . . 13 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑇))‘𝑛))
5352adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑇))‘𝑛))
541ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → 𝑁 ∈ ℕ)
55 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → (2nd𝑡) = (2nd𝑧))
5655breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑧)))
5756ifbid 4058 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)))
5857csbeq1d 3506 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
59 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → (1st𝑡) = (1st𝑧))
6059fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑧)))
6159fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑧 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑧)))
6261imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑧)) “ (1...𝑗)))
6362xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}))
6461imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)))
6564xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
6663, 65uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
6760, 66oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
6867csbeq2dv 3944 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
6958, 68eqtrd 2644 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
7069mpteq2dv 4673 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
7170eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
7271, 3elrab2 3333 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
7372simprbi 479 . . . . . . . . . . . . . . . 16 (𝑧𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
7473ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
75 elrabi 3328 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7675, 3eleq2s 2706 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
77 xp1st 7089 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7876, 77syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
79 xp1st 7089 . . . . . . . . . . . . . . . . . . 19 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
8078, 79syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
81 elmapi 7765 . . . . . . . . . . . . . . . . . 18 ((1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
8280, 81syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
83 fss 5969 . . . . . . . . . . . . . . . . 17 (((1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
8482, 41, 83sylancl 693 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
8584ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
86 xp2nd 7090 . . . . . . . . . . . . . . . . . 18 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
8778, 86syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
88 fvex 6113 . . . . . . . . . . . . . . . . . 18 (2nd ‘(1st𝑧)) ∈ V
89 f1oeq1 6040 . . . . . . . . . . . . . . . . . 18 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
9088, 89elab 3319 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
9187, 90sylib 207 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
9291ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
93 simpllr 795 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → (2nd𝑇) ∈ (1...(𝑁 − 1)))
94 xp2nd 7090 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑧) ∈ (0...𝑁))
9576, 94syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (2nd𝑧) ∈ (0...𝑁))
9695adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (2nd𝑧) ∈ (0...𝑁))
97 eldifsn 4260 . . . . . . . . . . . . . . . . 17 ((2nd𝑧) ∈ ((0...𝑁) ∖ {(2nd𝑇)}) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ (2nd𝑧) ≠ (2nd𝑇)))
9897biimpri 217 . . . . . . . . . . . . . . . 16 (((2nd𝑧) ∈ (0...𝑁) ∧ (2nd𝑧) ≠ (2nd𝑇)) → (2nd𝑧) ∈ ((0...𝑁) ∖ {(2nd𝑇)}))
9996, 98sylan 487 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → (2nd𝑧) ∈ ((0...𝑁) ∖ {(2nd𝑇)}))
10054, 74, 85, 92, 93, 99poimirlem2 32581 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) ≠ (2nd𝑇)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑇))‘𝑛))
101100ex 449 . . . . . . . . . . . . 13 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → ((2nd𝑧) ≠ (2nd𝑇) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑇))‘𝑛)))
102101necon1bd 2800 . . . . . . . . . . . 12 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑇))‘𝑛) → (2nd𝑧) = (2nd𝑇)))
10353, 102mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (2nd𝑧) = (2nd𝑇))
104 eleq1 2676 . . . . . . . . . . . . . . . 16 ((2nd𝑧) = (2nd𝑇) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ (2nd𝑇) ∈ (1...(𝑁 − 1))))
105104biimparc 503 . . . . . . . . . . . . . . 15 (((2nd𝑇) ∈ (1...(𝑁 − 1)) ∧ (2nd𝑧) = (2nd𝑇)) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
106105anim2i 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((2nd𝑇) ∈ (1...(𝑁 − 1)) ∧ (2nd𝑧) = (2nd𝑇))) → (𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))))
107106anassrs 678 . . . . . . . . . . . . 13 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑧) = (2nd𝑇)) → (𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))))
10873adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
109 breq1 4586 . . . . . . . . . . . . . . . . . 18 (𝑦 = 0 → (𝑦 < (2nd𝑧) ↔ 0 < (2nd𝑧)))
110 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = 0 → 𝑦 = 0)
111109, 110ifbieq1d 4059 . . . . . . . . . . . . . . . . 17 (𝑦 = 0 → if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2nd𝑧), 0, (𝑦 + 1)))
112 elfznn 12241 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ∈ ℕ)
113112nngt0d 10941 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2nd𝑧))
114113iftrued 4044 . . . . . . . . . . . . . . . . . 18 ((2nd𝑧) ∈ (1...(𝑁 − 1)) → if(0 < (2nd𝑧), 0, (𝑦 + 1)) = 0)
115114ad2antlr 759 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → if(0 < (2nd𝑧), 0, (𝑦 + 1)) = 0)
116111, 115sylan9eqr 2666 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) = 0)
117116csbeq1d 3506 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 0 / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
118 c0ex 9913 . . . . . . . . . . . . . . . . . 18 0 ∈ V
119 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (1...𝑗) = (1...0))
120 fz10 12233 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...0) = ∅
121119, 120syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → (1...𝑗) = ∅)
122121imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → ((2nd ‘(1st𝑧)) “ (1...𝑗)) = ((2nd ‘(1st𝑧)) “ ∅))
123122xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 0 → (((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑧)) “ ∅) × {1}))
124 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
125 0p1e1 11009 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
126124, 125syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑗 + 1) = 1)
127126oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
128127imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → ((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
129128xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 0 → (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}))
130123, 129uneq12d 3730 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 0 → ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ ∅) × {1}) ∪ (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})))
131 ima0 5400 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ‘(1st𝑧)) “ ∅) = ∅
132131xpeq1i 5059 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑧)) “ ∅) × {1}) = (∅ × {1})
133 0xp 5122 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ × {1}) = ∅
134132, 133eqtri 2632 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd ‘(1st𝑧)) “ ∅) × {1}) = ∅
135134uneq1i 3725 . . . . . . . . . . . . . . . . . . . . 21 ((((2nd ‘(1st𝑧)) “ ∅) × {1}) ∪ (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}))
136 uncom 3719 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∪ (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
137 un0 3919 . . . . . . . . . . . . . . . . . . . . 21 ((((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})
138135, 136, 1373eqtri 2636 . . . . . . . . . . . . . . . . . . . 20 ((((2nd ‘(1st𝑧)) “ ∅) × {1}) ∪ (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})) = (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})
139130, 138syl6eq 2660 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 → ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}))
140139oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 → ((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})))
141118, 140csbie 3525 . . . . . . . . . . . . . . . . 17 0 / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}))
142 f1ofo 6057 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
14391, 142syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
144 foima 6033 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
146145xpeq1d 5062 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆 → (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
147146oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → ((1st ‘(1st𝑧)) ∘𝑓 + (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})) = ((1st ‘(1st𝑧)) ∘𝑓 + ((1...𝑁) × {0})))
148 ovex 6577 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ∈ V
149148a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆 → (1...𝑁) ∈ V)
150 ffn 5958 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾) → (1st ‘(1st𝑧)) Fn (1...𝑁))
15182, 150syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆 → (1st ‘(1st𝑧)) Fn (1...𝑁))
152 fnconstg 6006 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
153118, 152mp1i 13 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
154 eqidd 2611 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑧))‘𝑛) = ((1st ‘(1st𝑧))‘𝑛))
155118fvconst2 6374 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
156155adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
15782ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑧))‘𝑛) ∈ (0..^𝐾))
158 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . 22 (((1st ‘(1st𝑧))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑧))‘𝑛) ∈ ℕ0)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑧))‘𝑛) ∈ ℕ0)
160159nn0cnd 11230 . . . . . . . . . . . . . . . . . . . 20 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑧))‘𝑛) ∈ ℂ)
161160addid1d 10115 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑧))‘𝑛) + 0) = ((1st ‘(1st𝑧))‘𝑛))
162149, 151, 153, 151, 154, 156, 161offveq 6816 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → ((1st ‘(1st𝑧)) ∘𝑓 + ((1...𝑁) × {0})) = (1st ‘(1st𝑧)))
163147, 162eqtrd 2644 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → ((1st ‘(1st𝑧)) ∘𝑓 + (((2nd ‘(1st𝑧)) “ (1...𝑁)) × {0})) = (1st ‘(1st𝑧)))
164141, 163syl5eq 2656 . . . . . . . . . . . . . . . 16 (𝑧𝑆0 / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st ‘(1st𝑧)))
165164ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑦 = 0) → 0 / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st ‘(1st𝑧)))
166117, 165eqtrd 2644 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st ‘(1st𝑧)))
167 nnm1nn0 11211 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
1681, 167syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℕ0)
169 0elfz 12305 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ ℕ0 → 0 ∈ (0...(𝑁 − 1)))
170168, 169syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ (0...(𝑁 − 1)))
171170ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → 0 ∈ (0...(𝑁 − 1)))
172 fvex 6113 . . . . . . . . . . . . . . 15 (1st ‘(1st𝑧)) ∈ V
173172a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (1st ‘(1st𝑧)) ∈ V)
174108, 166, 171, 173fvmptd 6197 . . . . . . . . . . . . 13 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝐹‘0) = (1st ‘(1st𝑧)))
175107, 174sylan 487 . . . . . . . . . . . 12 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑧) = (2nd𝑇)) ∧ 𝑧𝑆) → (𝐹‘0) = (1st ‘(1st𝑧)))
176175an32s 842 . . . . . . . . . . 11 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ (2nd𝑧) = (2nd𝑇)) → (𝐹‘0) = (1st ‘(1st𝑧)))
177103, 176mpdan 699 . . . . . . . . . 10 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝐹‘0) = (1st ‘(1st𝑧)))
178 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑇 → (2nd𝑧) = (2nd𝑇))
179178eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑧 = 𝑇 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ (2nd𝑇) ∈ (1...(𝑁 − 1))))
180179anbi2d 736 . . . . . . . . . . . . . 14 (𝑧 = 𝑇 → ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1)))))
181 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑇 → (1st𝑧) = (1st𝑇))
182181fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑧 = 𝑇 → (1st ‘(1st𝑧)) = (1st ‘(1st𝑇)))
183182eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑧 = 𝑇 → ((𝐹‘0) = (1st ‘(1st𝑧)) ↔ (𝐹‘0) = (1st ‘(1st𝑇))))
184180, 183imbi12d 333 . . . . . . . . . . . . 13 (𝑧 = 𝑇 → (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st ‘(1st𝑧))) ↔ ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st ‘(1st𝑇)))))
185174expcom 450 . . . . . . . . . . . . 13 (𝑧𝑆 → ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st ‘(1st𝑧))))
186184, 185vtoclga 3245 . . . . . . . . . . . 12 (𝑇𝑆 → ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st ‘(1st𝑇))))
1877, 186mpcom 37 . . . . . . . . . . 11 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st ‘(1st𝑇)))
188187adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝐹‘0) = (1st ‘(1st𝑇)))
189177, 188eqtr3d 2646 . . . . . . . . 9 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑇)))
190189adantr 480 . . . . . . . 8 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑇)))
1911ad3antrrr 762 . . . . . . . . 9 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → 𝑁 ∈ ℕ)
1926ad3antrrr 762 . . . . . . . . 9 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → 𝑇𝑆)
193 simpllr 795 . . . . . . . . 9 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (2nd𝑇) ∈ (1...(𝑁 − 1)))
194 simplr 788 . . . . . . . . 9 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → 𝑧𝑆)
19535adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
196 xpopth 7098 . . . . . . . . . . . . . 14 (((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑇))) ↔ (1st𝑧) = (1st𝑇)))
19778, 195, 196syl2anr 494 . . . . . . . . . . . . 13 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑇))) ↔ (1st𝑧) = (1st𝑇)))
19833adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
199 xpopth 7098 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑇) ∧ (2nd𝑧) = (2nd𝑇)) ↔ 𝑧 = 𝑇))
200199biimpd 218 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑇) ∧ (2nd𝑧) = (2nd𝑇)) → 𝑧 = 𝑇))
20176, 198, 200syl2anr 494 . . . . . . . . . . . . . 14 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (((1st𝑧) = (1st𝑇) ∧ (2nd𝑧) = (2nd𝑇)) → 𝑧 = 𝑇))
202103, 201mpan2d 706 . . . . . . . . . . . . 13 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → ((1st𝑧) = (1st𝑇) → 𝑧 = 𝑇))
203197, 202sylbid 229 . . . . . . . . . . . 12 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑇))) → 𝑧 = 𝑇))
204189, 203mpand 707 . . . . . . . . . . 11 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → ((2nd ‘(1st𝑧)) = (2nd ‘(1st𝑇)) → 𝑧 = 𝑇))
205204necon3d 2803 . . . . . . . . . 10 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝑧𝑇 → (2nd ‘(1st𝑧)) ≠ (2nd ‘(1st𝑇))))
206205imp 444 . . . . . . . . 9 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (2nd ‘(1st𝑧)) ≠ (2nd ‘(1st𝑇)))
207191, 3, 192, 193, 194, 206poimirlem9 32588 . . . . . . . 8 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
208103adantr 480 . . . . . . . 8 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (2nd𝑧) = (2nd𝑇))
209190, 207, 208jca31 555 . . . . . . 7 ((((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) ∧ 𝑧𝑇) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) ∧ (2nd𝑧) = (2nd𝑇)))
210209ex 449 . . . . . 6 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝑧𝑇 → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) ∧ (2nd𝑧) = (2nd𝑇))))
211 simplr 788 . . . . . . . 8 ((((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)})))))
212 elfznn 12241 . . . . . . . . . . . . . 14 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
213212nnred 10912 . . . . . . . . . . . . 13 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℝ)
214213ltp1d 10833 . . . . . . . . . . . . 13 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) < ((2nd𝑇) + 1))
215213, 214ltned 10052 . . . . . . . . . . . 12 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≠ ((2nd𝑇) + 1))
216215adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ≠ ((2nd𝑇) + 1))
217 fveq1 6102 . . . . . . . . . . . . 13 ((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𝑇)))
218 id 22 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd𝑇) ∈ ℝ → (2nd𝑇) ∈ ℝ)
219 ltp1 10740 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd𝑇) ∈ ℝ → (2nd𝑇) < ((2nd𝑇) + 1))
220218, 219ltned 10052 . . . . . . . . . . . . . . . . . . . . 21 ((2nd𝑇) ∈ ℝ → (2nd𝑇) ≠ ((2nd𝑇) + 1))
221 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑇) ∈ V
222 ovex 6577 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd𝑇) + 1) ∈ V
223221, 222, 222, 221fpr 6326 . . . . . . . . . . . . . . . . . . . . 21 ((2nd𝑇) ≠ ((2nd𝑇) + 1) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd𝑇) + 1), (2nd𝑇)})
224220, 223syl 17 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ ℝ → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd𝑇) + 1), (2nd𝑇)})
225 f1oi 6086 . . . . . . . . . . . . . . . . . . . . 21 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
226 f1of 6050 . . . . . . . . . . . . . . . . . . . . 21 (( 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)}))
227225, 226ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})⟶((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
228 disjdif 3992 . . . . . . . . . . . . . . . . . . . . 21 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅
229 fun 5979 . . . . . . . . . . . . . . . . . . . . 21 ((({⟨(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)})))
230228, 229mpan2 703 . . . . . . . . . . . . . . . . . . . 20 (({⟨(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)})))
231224, 227, 230sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((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)})))
232221prid1 4241 . . . . . . . . . . . . . . . . . . . 20 (2nd𝑇) ∈ {(2nd𝑇), ((2nd𝑇) + 1)}
233 elun1 3742 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ {(2nd𝑇), ((2nd𝑇) + 1)} → (2nd𝑇) ∈ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
234232, 233ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (2nd𝑇) ∈ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
235 fvco3 6185 . . . . . . . . . . . . . . . . . . 19 ((({⟨(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𝑇))))
236231, 234, 235sylancl 693 . . . . . . . . . . . . . . . . . 18 ((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𝑇))))
237 ffn 5958 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd𝑇) + 1), (2nd𝑇)} → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
238224, 237syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((2nd𝑇) ∈ ℝ → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
239 fnresi 5922 . . . . . . . . . . . . . . . . . . . . . 22 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
240228, 232pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅ ∧ (2nd𝑇) ∈ {(2nd𝑇), ((2nd𝑇) + 1)})
241 fvun1 6179 . . . . . . . . . . . . . . . . . . . . . 22 (({⟨(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𝑇)))
242239, 240, 241mp3an23 1408 . . . . . . . . . . . . . . . . . . . . 21 ({⟨(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𝑇)))
243238, 242syl 17 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ ℝ → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))‘(2nd𝑇)) = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}‘(2nd𝑇)))
244221, 222fvpr1 6361 . . . . . . . . . . . . . . . . . . . . 21 ((2nd𝑇) ≠ ((2nd𝑇) + 1) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}‘(2nd𝑇)) = ((2nd𝑇) + 1))
245220, 244syl 17 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ ℝ → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}‘(2nd𝑇)) = ((2nd𝑇) + 1))
246243, 245eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ ℝ → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))‘(2nd𝑇)) = ((2nd𝑇) + 1))
247246fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ((2nd𝑇) ∈ ℝ → ((2nd ‘(1st𝑇))‘(({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))‘(2nd𝑇))) = ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
248236, 247eqtrd 2644 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ ℝ → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))‘(2nd𝑇)) = ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
249213, 248syl 17 . . . . . . . . . . . . . . . 16 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))‘(2nd𝑇)) = ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
250249eqeq2d 2620 . . . . . . . . . . . . . . 15 ((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))))
251250adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (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))))
252 f1of1 6049 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁))
25350, 252syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁))
254253adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁))
2551nncnd 10913 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
256 npcan1 10334 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
257255, 256syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
258168nn0zd 11356 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁 − 1) ∈ ℤ)
259 uzid 11578 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
260258, 259syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
261 peano2uz 11617 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
262260, 261syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
263257, 262eqeltrrd 2689 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
264 fzss2 12252 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
265263, 264syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
266265sselda 3568 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ∈ (1...𝑁))
267 fzp1elp1 12264 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
268267adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
269257oveq2d 6565 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
270269adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
271268, 270eleqtrd 2690 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) + 1) ∈ (1...𝑁))
272 f1veqaeq 6418 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ ((2nd𝑇) ∈ (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁))) → (((2nd ‘(1st𝑇))‘(2nd𝑇)) = ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) → (2nd𝑇) = ((2nd𝑇) + 1)))
273254, 266, 271, 272syl12anc 1316 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (((2nd ‘(1st𝑇))‘(2nd𝑇)) = ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) → (2nd𝑇) = ((2nd𝑇) + 1)))
274251, 273sylbid 229 . . . . . . . . . . . . 13 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (((2nd ‘(1st𝑇))‘(2nd𝑇)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))‘(2nd𝑇)) → (2nd𝑇) = ((2nd𝑇) + 1)))
275217, 274syl5 33 . . . . . . . . . . . 12 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → (2nd𝑇) = ((2nd𝑇) + 1)))
276275necon3d 2803 . . . . . . . . . . 11 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ ((2nd𝑇) + 1) → (2nd ‘(1st𝑇)) ≠ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))))
277216, 276mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑇)) ≠ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
278181fveq2d 6107 . . . . . . . . . . 11 (𝑧 = 𝑇 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑇)))
279278neeq1d 2841 . . . . . . . . . 10 (𝑧 = 𝑇 → ((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)}))))))
280277, 279syl5ibrcom 236 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → (𝑧 = 𝑇 → (2nd ‘(1st𝑧)) ≠ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))))
281280necon2d 2805 . . . . . . . 8 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → 𝑧𝑇))
282211, 281syl5 33 . . . . . . 7 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) ∧ (2nd𝑧) = (2nd𝑇)) → 𝑧𝑇))
283282adantr 480 . . . . . 6 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → ((((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) ∧ (2nd𝑧) = (2nd𝑇)) → 𝑧𝑇))
284210, 283impbid 201 . . . . 5 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝑧𝑇 ↔ (((1st ‘(1st𝑧)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑧)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) ∧ (2nd𝑧) = (2nd𝑇))))
285 eqop 7099 . . . . . . . 8 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (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𝑇))))
286 eqop 7099 . . . . . . . . . 10 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (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)})))))))
28777, 286syl 17 . . . . . . . . 9 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (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)})))))))
288287anbi1d 737 . . . . . . . 8 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (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𝑇))))
289285, 288bitrd 267 . . . . . . 7 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (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𝑇))))
29076, 289syl 17 . . . . . 6 (𝑧𝑆 → (𝑧 = ⟨⟨(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𝑇))))
291290adantl 481 . . . . 5 (((𝜑 ∧ (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𝑇))))
292284, 291bitr4d 270 . . . 4 (((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧𝑆) → (𝑧𝑇𝑧 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩))
293292ralrimiva 2949 . . 3 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ∀𝑧𝑆 (𝑧𝑇𝑧 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩))
294 reu6i 3364 . . 3 ((⟨⟨(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𝑇)⟩)) → ∃!𝑧𝑆 𝑧𝑇)
2959, 293, 294syl2anc 691 . 2 ((𝜑 ∧ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧𝑆 𝑧𝑇)
296 xp2nd 7090 . . . . . . 7 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑇) ∈ (0...𝑁))
29733, 296syl 17 . . . . . 6 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
298297biantrurd 528 . . . . 5 (𝜑 → (¬ (2nd𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2nd𝑇) ∈ (0...𝑁) ∧ ¬ (2nd𝑇) ∈ (1...(𝑁 − 1)))))
2991nnnn0d 11228 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
300 nn0uz 11598 . . . . . . . . . . . 12 0 = (ℤ‘0)
301299, 300syl6eleq 2698 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘0))
302 fzpred 12259 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
303301, 302syl 17 . . . . . . . . . 10 (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
304125oveq1i 6559 . . . . . . . . . . 11 ((0 + 1)...𝑁) = (1...𝑁)
305304uneq2i 3726 . . . . . . . . . 10 ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
306303, 305syl6eq 2660 . . . . . . . . 9 (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
307306difeq1d 3689 . . . . . . . 8 (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
308 difundir 3839 . . . . . . . . . 10 (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
309 0lt1 10429 . . . . . . . . . . . . . 14 0 < 1
310 0re 9919 . . . . . . . . . . . . . . 15 0 ∈ ℝ
311 1re 9918 . . . . . . . . . . . . . . 15 1 ∈ ℝ
312310, 311ltnlei 10037 . . . . . . . . . . . . . 14 (0 < 1 ↔ ¬ 1 ≤ 0)
313309, 312mpbi 219 . . . . . . . . . . . . 13 ¬ 1 ≤ 0
314 elfzle1 12215 . . . . . . . . . . . . 13 (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
315313, 314mto 187 . . . . . . . . . . . 12 ¬ 0 ∈ (1...(𝑁 − 1))
316 incom 3767 . . . . . . . . . . . . . 14 ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
317316eqeq1i 2615 . . . . . . . . . . . . 13 (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
318 disjsn 4192 . . . . . . . . . . . . 13 (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
319 disj3 3973 . . . . . . . . . . . . 13 (({0} ∩ (1...(𝑁 − 1))) = ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
320317, 318, 3193bitr3i 289 . . . . . . . . . . . 12 (¬ 0 ∈ (1...(𝑁 − 1)) ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
321315, 320mpbi 219 . . . . . . . . . . 11 {0} = ({0} ∖ (1...(𝑁 − 1)))
322321uneq1i 3725 . . . . . . . . . 10 ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
323308, 322eqtr4i 2635 . . . . . . . . 9 (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
324 difundir 3839 . . . . . . . . . . . 12 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
325 difid 3902 . . . . . . . . . . . . 13 ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
326325uneq1i 3725 . . . . . . . . . . . 12 (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
327 uncom 3719 . . . . . . . . . . . . 13 (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
328 un0 3919 . . . . . . . . . . . . 13 (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
329327, 328eqtri 2632 . . . . . . . . . . . 12 (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
330324, 326, 3293eqtri 2636 . . . . . . . . . . 11 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
331 nnuz 11599 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
3321, 331syl6eleq 2698 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ (ℤ‘1))
333257, 332eqeltrd 2688 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
334 fzsplit2 12237 . . . . . . . . . . . . . 14 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
335333, 263, 334syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
336257oveq1d 6564 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
3371nnzd 11357 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
338 fzsn 12254 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
339337, 338syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁...𝑁) = {𝑁})
340336, 339eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
341340uneq2d 3729 . . . . . . . . . . . . 13 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
342335, 341eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
343342difeq1d 3689 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
3441nnred 10912 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
345344ltm1d 10835 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) < 𝑁)
346168nn0red 11229 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − 1) ∈ ℝ)
347346, 344ltnled 10063 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
348345, 347mpbid 221 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
349 elfzle2 12216 . . . . . . . . . . . . 13 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
350348, 349nsyl 134 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
351 incom 3767 . . . . . . . . . . . . . 14 ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
352351eqeq1i 2615 . . . . . . . . . . . . 13 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
353 disjsn 4192 . . . . . . . . . . . . 13 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
354 disj3 3973 . . . . . . . . . . . . 13 (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
355352, 353, 3543bitr3i 289 . . . . . . . . . . . 12 𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
356350, 355sylib 207 . . . . . . . . . . 11 (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
357330, 343, 3563eqtr4a 2670 . . . . . . . . . 10 (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
358357uneq2d 3729 . . . . . . . . 9 (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
359323, 358syl5eq 2656 . . . . . . . 8 (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
360307, 359eqtrd 2644 . . . . . . 7 (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
361360eleq2d 2673 . . . . . 6 (𝜑 → ((2nd𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2nd𝑇) ∈ ({0} ∪ {𝑁})))
362 eldif 3550 . . . . . 6 ((2nd𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2nd𝑇) ∈ (0...𝑁) ∧ ¬ (2nd𝑇) ∈ (1...(𝑁 − 1))))
363 elun 3715 . . . . . . 7 ((2nd𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2nd𝑇) ∈ {0} ∨ (2nd𝑇) ∈ {𝑁}))
364221elsn 4140 . . . . . . . 8 ((2nd𝑇) ∈ {0} ↔ (2nd𝑇) = 0)
365221elsn 4140 . . . . . . . 8 ((2nd𝑇) ∈ {𝑁} ↔ (2nd𝑇) = 𝑁)
366364, 365orbi12i 542 . . . . . . 7 (((2nd𝑇) ∈ {0} ∨ (2nd𝑇) ∈ {𝑁}) ↔ ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁))
367363, 366bitri 263 . . . . . 6 ((2nd𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁))
368361, 362, 3673bitr3g 301 . . . . 5 (𝜑 → (((2nd𝑇) ∈ (0...𝑁) ∧ ¬ (2nd𝑇) ∈ (1...(𝑁 − 1))) ↔ ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁)))
369298, 368bitrd 267 . . . 4 (𝜑 → (¬ (2nd𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁)))
370369biimpa 500 . . 3 ((𝜑 ∧ ¬ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁))
3711adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 0) → 𝑁 ∈ ℕ)
3724adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
3736adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 0) → 𝑇𝑆)
374 poimirlem22.4 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
375374adantlr 747 . . . . 5 (((𝜑 ∧ (2nd𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
376 simpr 476 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 0) → (2nd𝑇) = 0)
377371, 3, 372, 373, 375, 376poimirlem18 32597 . . . 4 ((𝜑 ∧ (2nd𝑇) = 0) → ∃!𝑧𝑆 𝑧𝑇)
3781adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 𝑁) → 𝑁 ∈ ℕ)
3794adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
3806adantr 480 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 𝑁) → 𝑇𝑆)
381 poimirlem22.3 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)
382381adantlr 747 . . . . 5 (((𝜑 ∧ (2nd𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)
383 simpr 476 . . . . 5 ((𝜑 ∧ (2nd𝑇) = 𝑁) → (2nd𝑇) = 𝑁)
384378, 3, 379, 380, 382, 383poimirlem21 32600 . . . 4 ((𝜑 ∧ (2nd𝑇) = 𝑁) → ∃!𝑧𝑆 𝑧𝑇)
385377, 384jaodan 822 . . 3 ((𝜑 ∧ ((2nd𝑇) = 0 ∨ (2nd𝑇) = 𝑁)) → ∃!𝑧𝑆 𝑧𝑇)
386370, 385syldan 486 . 2 ((𝜑 ∧ ¬ (2nd𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧𝑆 𝑧𝑇)
387295, 386pm2.61dan 828 1 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899  {crab 2900  Vcvv 3173  ⦋csb 3499   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125  {cpr 4127  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643   I cid 4948   × cxp 5036  ran crn 5039   ↾ cres 5040   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ..^cfzo 12334 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-fac 12923  df-bc 12952  df-hash 12980 This theorem is referenced by:  poimirlem27  32606
 Copyright terms: Public domain W3C validator