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

Theorem poimirlem21 33749
Description: Lemma for poimir 33761 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.)
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)
poimirlem21.4 (𝜑 → (2nd𝑇) = 𝑁)
Assertion
Ref Expression
poimirlem21 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
Distinct variable groups:   𝑓,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑝,𝑡   𝑓,𝐾,𝑗,𝑛,𝑝,𝑡   𝑓,𝑁,𝑝,𝑡   𝑇,𝑓,𝑝   𝜑,𝑧   𝑓,𝐹,𝑝,𝑡,𝑧   𝑧,𝐾   𝑧,𝑁   𝑡,𝑇,𝑧   𝑆,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem21
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . 3 (𝜑𝑁 ∈ ℕ)
2 poimirlem22.s . . 3 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
3 poimirlem22.1 . . 3 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
4 poimirlem22.2 . . 3 (𝜑𝑇𝑆)
5 poimirlem22.3 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 0)
6 poimirlem21.4 . . 3 (𝜑 → (2nd𝑇) = 𝑁)
71, 2, 3, 4, 5, 6poimirlem20 33748 . 2 (𝜑 → ∃𝑧𝑆 𝑧𝑇)
86adantr 468 . . . . . . . 8 ((𝜑𝑧𝑆) → (2nd𝑇) = 𝑁)
91nnred 11327 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
109ltm1d 11248 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − 1) < 𝑁)
11 nnm1nn0 11607 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
121, 11syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ ℕ0)
1312nn0red 11625 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
1413, 9ltnled 10476 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
1510, 14mpbid 223 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
16 elfzle2 12575 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
1715, 16nsyl 137 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
18 eleq1 2884 . . . . . . . . . . . . . 14 ((2nd𝑧) = 𝑁 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
1918notbid 309 . . . . . . . . . . . . 13 ((2nd𝑧) = 𝑁 → (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
2017, 19syl5ibrcom 238 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑧) = 𝑁 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
2120necon2ad 3004 . . . . . . . . . . 11 (𝜑 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ≠ 𝑁))
2221adantr 468 . . . . . . . . . 10 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ≠ 𝑁))
231ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
24 fveq2 6415 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (2nd𝑡) = (2nd𝑧))
2524breq2d 4867 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑧)))
2625ifbid 4312 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)))
2726csbeq1d 3746 . . . . . . . . . . . . . . . . . . . 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}))))
28 2fveq3 6420 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑧)))
29 2fveq3 6420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑧 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑧)))
3029imaeq1d 5686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑧)) “ (1...𝑗)))
3130xpeq1d 5350 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}))
3229imaeq1d 5686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)))
3332xpeq1d 5350 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
3431, 33uneq12d 3978 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
3528, 34oveq12d 6899 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
3635csbeq2dv 4200 . . . . . . . . . . . . . . . . . . . 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}))))
3727, 36eqtrd 2851 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧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}))))
3837mpteq2dv 4950 . . . . . . . . . . . . . . . . . 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})))))
3938eqeq2d 2827 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (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}))))))
4039, 2elrab2 3573 . . . . . . . . . . . . . . . 16 (𝑧𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
4140simprbi 486 . . . . . . . . . . . . . . 15 (𝑧𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
4241ad2antlr 709 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
43 elrabi 3565 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑡 ∈ ((((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...𝑁)))
4443, 2eleq2s 2914 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
45 xp1st 7437 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
4644, 45syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
47 xp1st 7437 . . . . . . . . . . . . . . . . . 18 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
4846, 47syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
49 elmapi 8121 . . . . . . . . . . . . . . . . 17 ((1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
5048, 49syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
51 elfzoelz 12701 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
5251ssriv 3813 . . . . . . . . . . . . . . . 16 (0..^𝐾) ⊆ ℤ
53 fss 6276 . . . . . . . . . . . . . . . 16 (((1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
5450, 52, 53sylancl 576 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
5554ad2antlr 709 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
56 xp2nd 7438 . . . . . . . . . . . . . . . . 17 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5746, 56syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 fvex 6428 . . . . . . . . . . . . . . . . 17 (2nd ‘(1st𝑧)) ∈ V
59 f1oeq1 6350 . . . . . . . . . . . . . . . . 17 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
6058, 59elab 3556 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
6157, 60sylib 209 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
6261ad2antlr 709 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
63 simpr 473 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
6423, 42, 55, 62, 63poimirlem1 33729 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
651ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝑁 ∈ ℕ)
66 fveq2 6415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
6766breq2d 4867 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
6867ifbid 4312 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
6968csbeq1d 3746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇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}))))
70 2fveq3 6420 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
71 2fveq3 6420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
7271imaeq1d 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
7372xpeq1d 5350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
7471imaeq1d 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
7574xpeq1d 5350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
7673, 75uneq12d 3978 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
7770, 76oveq12d 6899 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
7877csbeq2dv 4200 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑇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}))))
7969, 78eqtrd 2851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑇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}))))
8079mpteq2dv 4950 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑇 → (𝑦 ∈ (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})))))
8180eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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}))))))
8281, 2elrab2 3573 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
8382simprbi 486 . . . . . . . . . . . . . . . . . . 19 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
844, 83syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
8584ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
86 elrabi 3565 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑇 ∈ {𝑡 ∈ ((((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...𝑁)))
8786, 2eleq2s 2914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
884, 87syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
89 xp1st 7437 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
91 xp1st 7437 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
93 elmapi 8121 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
9492, 93syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
95 fss 6276 . . . . . . . . . . . . . . . . . . 19 (((1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9694, 52, 95sylancl 576 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9796ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
98 xp2nd 7438 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
9990, 98syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
100 fvex 6428 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
101 f1oeq1 6350 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
102100, 101elab 3556 . . . . . . . . . . . . . . . . . . 19 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
10399, 102sylib 209 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
104103ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
105 simplr 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
106 xp2nd 7438 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑇) ∈ (0...𝑁))
10788, 106syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
108107adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ∈ (0...𝑁))
109 eldifsn 4519 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}) ↔ ((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)))
110109biimpri 219 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
111108, 110sylan 571 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
11265, 85, 97, 104, 105, 111poimirlem2 33730 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
113112ex 399 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ (2nd𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛)))
114113necon1bd 3007 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
115114adantlr 697 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
11664, 115mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) = (2nd𝑧))
117116neeq1d 3048 . . . . . . . . . . 11 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ 𝑁 ↔ (2nd𝑧) ≠ 𝑁))
118117exbiri 836 . . . . . . . . . 10 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → ((2nd𝑧) ≠ 𝑁 → (2nd𝑇) ≠ 𝑁)))
11922, 118mpdd 43 . . . . . . . . 9 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≠ 𝑁))
120119necon2bd 3005 . . . . . . . 8 ((𝜑𝑧𝑆) → ((2nd𝑇) = 𝑁 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
1218, 120mpd 15 . . . . . . 7 ((𝜑𝑧𝑆) → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))
122 xp2nd 7438 . . . . . . . . 9 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑧) ∈ (0...𝑁))
12344, 122syl 17 . . . . . . . 8 (𝑧𝑆 → (2nd𝑧) ∈ (0...𝑁))
124 nn0uz 11947 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
12512, 124syl6eleq 2906 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ (ℤ‘0))
126 fzpred 12619 . . . . . . . . . . . . . . . . 17 ((𝑁 − 1) ∈ (ℤ‘0) → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1))))
127125, 126syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1))))
128 0p1e1 11421 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
129128oveq1i 6891 . . . . . . . . . . . . . . . . 17 ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
130129uneq2i 3974 . . . . . . . . . . . . . . . 16 ({0} ∪ ((0 + 1)...(𝑁 − 1))) = ({0} ∪ (1...(𝑁 − 1)))
131127, 130syl6eq 2867 . . . . . . . . . . . . . . 15 (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ (1...(𝑁 − 1))))
132131eleq2d 2882 . . . . . . . . . . . . . 14 (𝜑 → ((2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1)))))
133132notbid 309 . . . . . . . . . . . . 13 (𝜑 → (¬ (2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ ¬ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1)))))
134 ioran 997 . . . . . . . . . . . . . 14 (¬ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
135 elun 3963 . . . . . . . . . . . . . . 15 ((2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ {0} ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
136 fvex 6428 . . . . . . . . . . . . . . . . 17 (2nd𝑧) ∈ V
137136elsn 4396 . . . . . . . . . . . . . . . 16 ((2nd𝑧) ∈ {0} ↔ (2nd𝑧) = 0)
138137orbi1i 928 . . . . . . . . . . . . . . 15 (((2nd𝑧) ∈ {0} ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))) ↔ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
139135, 138bitri 266 . . . . . . . . . . . . . 14 ((2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
140134, 139xchnxbir 324 . . . . . . . . . . . . 13 (¬ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
141133, 140syl6bb 278 . . . . . . . . . . . 12 (𝜑 → (¬ (2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))))
142141anbi2d 616 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))))
143 uncom 3967 . . . . . . . . . . . . . . . 16 ((0...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ (0...(𝑁 − 1)))
144143difeq1i 3934 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))) = (({𝑁} ∪ (0...(𝑁 − 1))) ∖ (0...(𝑁 − 1)))
145 difun2 4255 . . . . . . . . . . . . . . 15 (({𝑁} ∪ (0...(𝑁 − 1))) ∖ (0...(𝑁 − 1))) = ({𝑁} ∖ (0...(𝑁 − 1)))
146144, 145eqtri 2839 . . . . . . . . . . . . . 14 (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))) = ({𝑁} ∖ (0...(𝑁 − 1)))
1471nncnd 11328 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
148 npcan1 10747 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
149147, 148syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1501nnnn0d 11624 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
151150, 124syl6eleq 2906 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
152149, 151eqeltrd 2896 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘0))
15312nn0zd 11753 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) ∈ ℤ)
154 uzid 11926 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
155 peano2uz 11966 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
156153, 154, 1553syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
157149, 156eqeltrrd 2897 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
158 fzsplit2 12596 . . . . . . . . . . . . . . . . 17 ((((𝑁 − 1) + 1) ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
159152, 157, 158syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
160149oveq1d 6896 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
1611nnzd 11754 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
162 fzsn 12613 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
163161, 162syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁...𝑁) = {𝑁})
164160, 163eqtrd 2851 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
165164uneq2d 3977 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((0...(𝑁 − 1)) ∪ {𝑁}))
166159, 165eqtrd 2851 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ {𝑁}))
167166difeq1d 3937 . . . . . . . . . . . . . 14 (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))))
168 elfzle2 12575 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (0...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
16915, 168nsyl 137 . . . . . . . . . . . . . . 15 (𝜑 → ¬ 𝑁 ∈ (0...(𝑁 − 1)))
170 incom 4015 . . . . . . . . . . . . . . . . 17 ((0...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (0...(𝑁 − 1)))
171170eqeq1i 2822 . . . . . . . . . . . . . . . 16 (((0...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (0...(𝑁 − 1))) = ∅)
172 disjsn 4449 . . . . . . . . . . . . . . . 16 (((0...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (0...(𝑁 − 1)))
173 disj3 4229 . . . . . . . . . . . . . . . 16 (({𝑁} ∩ (0...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
174171, 172, 1733bitr3i 292 . . . . . . . . . . . . . . 15 𝑁 ∈ (0...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
175169, 174sylib 209 . . . . . . . . . . . . . 14 (𝜑 → {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
176146, 167, 1753eqtr4a 2877 . . . . . . . . . . . . 13 (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = {𝑁})
177176eleq2d 2882 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑧) ∈ ((0...𝑁) ∖ (0...(𝑁 − 1))) ↔ (2nd𝑧) ∈ {𝑁}))
178 eldif 3790 . . . . . . . . . . . 12 ((2nd𝑧) ∈ ((0...𝑁) ∖ (0...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))))
179136elsn 4396 . . . . . . . . . . . 12 ((2nd𝑧) ∈ {𝑁} ↔ (2nd𝑧) = 𝑁)
180177, 178, 1793bitr3g 304 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))) ↔ (2nd𝑧) = 𝑁))
181142, 180bitr3d 272 . . . . . . . . . 10 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))) ↔ (2nd𝑧) = 𝑁))
182181biimpd 220 . . . . . . . . 9 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))) → (2nd𝑧) = 𝑁))
183182expdimp 442 . . . . . . . 8 ((𝜑 ∧ (2nd𝑧) ∈ (0...𝑁)) → ((¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) = 𝑁))
184123, 183sylan2 582 . . . . . . 7 ((𝜑𝑧𝑆) → ((¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) = 𝑁))
185121, 184mpan2d 677 . . . . . 6 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 0 → (2nd𝑧) = 𝑁))
1861, 2, 3poimirlem14 33742 . . . . . . . . . 10 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
187 fveqeq2 6424 . . . . . . . . . . 11 (𝑧 = 𝑠 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑠) = 𝑁))
188187rmo4 3608 . . . . . . . . . 10 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
189186, 188sylib 209 . . . . . . . . 9 (𝜑 → ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
190189r19.21bi 3131 . . . . . . . 8 ((𝜑𝑧𝑆) → ∀𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
1914adantr 468 . . . . . . . 8 ((𝜑𝑧𝑆) → 𝑇𝑆)
192 fveqeq2 6424 . . . . . . . . . . 11 (𝑠 = 𝑇 → ((2nd𝑠) = 𝑁 ↔ (2nd𝑇) = 𝑁))
193192anbi2d 616 . . . . . . . . . 10 (𝑠 = 𝑇 → (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) ↔ ((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁)))
194 eqeq2 2828 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝑧 = 𝑠𝑧 = 𝑇))
195193, 194imbi12d 335 . . . . . . . . 9 (𝑠 = 𝑇 → ((((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠) ↔ (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇)))
196195rspccv 3510 . . . . . . . 8 (∀𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠) → (𝑇𝑆 → (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇)))
197190, 191, 196sylc 65 . . . . . . 7 ((𝜑𝑧𝑆) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇))
1988, 197mpan2d 677 . . . . . 6 ((𝜑𝑧𝑆) → ((2nd𝑧) = 𝑁𝑧 = 𝑇))
199185, 198syld 47 . . . . 5 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 0 → 𝑧 = 𝑇))
200199necon1ad 3006 . . . 4 ((𝜑𝑧𝑆) → (𝑧𝑇 → (2nd𝑧) = 0))
201200ralrimiva 3165 . . 3 (𝜑 → ∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 0))
2021, 2, 3poimirlem13 33741 . . 3 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 0)
203 rmoim 3616 . . 3 (∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 0) → (∃*𝑧𝑆 (2nd𝑧) = 0 → ∃*𝑧𝑆 𝑧𝑇))
204201, 202, 203sylc 65 . 2 (𝜑 → ∃*𝑧𝑆 𝑧𝑇)
205 reu5 3359 . 2 (∃!𝑧𝑆 𝑧𝑇 ↔ (∃𝑧𝑆 𝑧𝑇 ∧ ∃*𝑧𝑆 𝑧𝑇))
2067, 204, 205sylanbrc 574 1 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 865   = wceq 1637  wcel 2157  {cab 2803  wne 2989  wral 3107  wrex 3108  ∃!wreu 3109  ∃*wrmo 3110  {crab 3111  csb 3739  cdif 3777  cun 3778  cin 3779  wss 3780  c0 4127  ifcif 4290  {csn 4381   class class class wbr 4855  cmpt 4934   × cxp 5320  ran crn 5323  cima 5325  wf 6104  1-1-ontowf1o 6107  cfv 6108  (class class class)co 6881  𝑓 cof 7132  1st c1st 7403  2nd c2nd 7404  𝑚 cmap 8099  cc 10226  0cc0 10228  1c1 10229   + caddc 10231   < clt 10366  cle 10367  cmin 10558  cn 11312  0cn0 11566  cz 11650  cuz 11911  ...cfz 12556  ..^cfzo 12696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-of 7134  df-om 7303  df-1st 7405  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-er 7986  df-map 8101  df-en 8200  df-dom 8201  df-sdom 8202  df-fin 8203  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-sub 10560  df-neg 10561  df-nn 11313  df-n0 11567  df-z 11651  df-uz 11912  df-fz 12557  df-fzo 12697
This theorem is referenced by:  poimirlem22  33750
  Copyright terms: Public domain W3C validator