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 33761
Description: Lemma for poimir 33773 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 33760 . 2 (𝜑 → ∃𝑧𝑆 𝑧𝑇)
86adantr 472 . . . . . . . 8 ((𝜑𝑧𝑆) → (2nd𝑇) = 𝑁)
91nnred 11247 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
109ltm1d 11168 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − 1) < 𝑁)
11 nnm1nn0 11546 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
121, 11syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ ℕ0)
1312nn0red 11564 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
1413, 9ltnled 10396 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
1510, 14mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
16 elfzle2 12558 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
1715, 16nsyl 135 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
18 eleq1 2827 . . . . . . . . . . . . . 14 ((2nd𝑧) = 𝑁 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
1918notbid 307 . . . . . . . . . . . . 13 ((2nd𝑧) = 𝑁 → (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
2017, 19syl5ibrcom 237 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑧) = 𝑁 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
2120necon2ad 2947 . . . . . . . . . . 11 (𝜑 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ≠ 𝑁))
2221adantr 472 . . . . . . . . . 10 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ≠ 𝑁))
231ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
24 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (2nd𝑡) = (2nd𝑧))
2524breq2d 4816 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑧)))
2625ifbid 4252 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)))
2726csbeq1d 3681 . . . . . . . . . . . . . . . . . . . 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 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (1st𝑡) = (1st𝑧))
2928fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑧)))
3028fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑧 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑧)))
3130imaeq1d 5623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑧)) “ (1...𝑗)))
3231xpeq1d 5295 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}))
3330imaeq1d 5623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)))
3433xpeq1d 5295 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
3532, 34uneq12d 3911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
3629, 35oveq12d 6832 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
3736csbeq2dv 4135 . . . . . . . . . . . . . . . . . . . 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}))))
3827, 37eqtrd 2794 . . . . . . . . . . . . . . . . . . 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}))))
3938mpteq2dv 4897 . . . . . . . . . . . . . . . . . 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})))))
4039eqeq2d 2770 . . . . . . . . . . . . . . . . 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}))))))
4140, 2elrab2 3507 . . . . . . . . . . . . . . . 16 (𝑧𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
4241simprbi 483 . . . . . . . . . . . . . . 15 (𝑧𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
4342ad2antlr 765 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
44 elrabi 3499 . . . . . . . . . . . . . . . . . . . 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...𝑁)))
4544, 2eleq2s 2857 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
46 xp1st 7366 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
4745, 46syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
48 xp1st 7366 . . . . . . . . . . . . . . . . . 18 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
4947, 48syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
50 elmapi 8047 . . . . . . . . . . . . . . . . 17 ((1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
5149, 50syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
52 elfzoelz 12684 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
5352ssriv 3748 . . . . . . . . . . . . . . . 16 (0..^𝐾) ⊆ ℤ
54 fss 6217 . . . . . . . . . . . . . . . 16 (((1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
5551, 53, 54sylancl 697 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
5655ad2antlr 765 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
57 xp2nd 7367 . . . . . . . . . . . . . . . . 17 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5847, 57syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
59 fvex 6363 . . . . . . . . . . . . . . . . 17 (2nd ‘(1st𝑧)) ∈ V
60 f1oeq1 6289 . . . . . . . . . . . . . . . . 17 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
6159, 60elab 3490 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
6258, 61sylib 208 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
6362ad2antlr 765 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
64 simpr 479 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
6523, 43, 56, 63, 64poimirlem1 33741 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
661ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝑁 ∈ ℕ)
67 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
6867breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
6968ifbid 4252 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
7069csbeq1d 3681 . . . . . . . . . . . . . . . . . . . . . . . 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}))))
71 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
7271fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
7371fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
7473imaeq1d 5623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
7574xpeq1d 5295 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
7673imaeq1d 5623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
7776xpeq1d 5295 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
7875, 77uneq12d 3911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
7972, 78oveq12d 6832 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
8079csbeq2dv 4135 . . . . . . . . . . . . . . . . . . . . . . . 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}))))
8170, 80eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . 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}))))
8281mpteq2dv 4897 . . . . . . . . . . . . . . . . . . . . . 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})))))
8382eqeq2d 2770 . . . . . . . . . . . . . . . . . . . . 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}))))))
8483, 2elrab2 3507 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
8584simprbi 483 . . . . . . . . . . . . . . . . . . 19 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
864, 85syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
8786ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
88 elrabi 3499 . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁)))
8988, 2eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
904, 89syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
91 xp1st 7366 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
93 xp1st 7366 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
95 elmapi 8047 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
97 fss 6217 . . . . . . . . . . . . . . . . . . 19 (((1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9896, 53, 97sylancl 697 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9998ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
100 xp2nd 7367 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10192, 100syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
102 fvex 6363 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
103 f1oeq1 6289 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
104102, 103elab 3490 . . . . . . . . . . . . . . . . . . 19 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
105101, 104sylib 208 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
106105ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
107 simplr 809 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
108 xp2nd 7367 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑇) ∈ (0...𝑁))
10990, 108syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
110109adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ∈ (0...𝑁))
111 eldifsn 4462 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}) ↔ ((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)))
112111biimpri 218 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
113110, 112sylan 489 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
11466, 87, 99, 106, 107, 113poimirlem2 33742 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
115114ex 449 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ (2nd𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛)))
116115necon1bd 2950 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
117116adantlr 753 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
11865, 117mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) = (2nd𝑧))
119118neeq1d 2991 . . . . . . . . . . 11 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ 𝑁 ↔ (2nd𝑧) ≠ 𝑁))
120119exbiri 653 . . . . . . . . . 10 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → ((2nd𝑧) ≠ 𝑁 → (2nd𝑇) ≠ 𝑁)))
12122, 120mpdd 43 . . . . . . . . 9 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≠ 𝑁))
122121necon2bd 2948 . . . . . . . 8 ((𝜑𝑧𝑆) → ((2nd𝑇) = 𝑁 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
1238, 122mpd 15 . . . . . . 7 ((𝜑𝑧𝑆) → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))
124 xp2nd 7367 . . . . . . . . 9 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑧) ∈ (0...𝑁))
12545, 124syl 17 . . . . . . . 8 (𝑧𝑆 → (2nd𝑧) ∈ (0...𝑁))
126 nn0uz 11935 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
12712, 126syl6eleq 2849 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 1) ∈ (ℤ‘0))
128 fzpred 12602 . . . . . . . . . . . . . . . . 17 ((𝑁 − 1) ∈ (ℤ‘0) → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1))))
129127, 128syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1))))
130 0p1e1 11344 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
131130oveq1i 6824 . . . . . . . . . . . . . . . . 17 ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
132131uneq2i 3907 . . . . . . . . . . . . . . . 16 ({0} ∪ ((0 + 1)...(𝑁 − 1))) = ({0} ∪ (1...(𝑁 − 1)))
133129, 132syl6eq 2810 . . . . . . . . . . . . . . 15 (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ (1...(𝑁 − 1))))
134133eleq2d 2825 . . . . . . . . . . . . . 14 (𝜑 → ((2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1)))))
135134notbid 307 . . . . . . . . . . . . 13 (𝜑 → (¬ (2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ ¬ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1)))))
136 ioran 512 . . . . . . . . . . . . . 14 (¬ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
137 elun 3896 . . . . . . . . . . . . . . 15 ((2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ {0} ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
138 fvex 6363 . . . . . . . . . . . . . . . . 17 (2nd𝑧) ∈ V
139138elsn 4336 . . . . . . . . . . . . . . . 16 ((2nd𝑧) ∈ {0} ↔ (2nd𝑧) = 0)
140139orbi1i 543 . . . . . . . . . . . . . . 15 (((2nd𝑧) ∈ {0} ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))) ↔ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
141137, 140bitri 264 . . . . . . . . . . . . . 14 ((2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd𝑧) = 0 ∨ (2nd𝑧) ∈ (1...(𝑁 − 1))))
142136, 141xchnxbir 322 . . . . . . . . . . . . 13 (¬ (2nd𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
143135, 142syl6bb 276 . . . . . . . . . . . 12 (𝜑 → (¬ (2nd𝑧) ∈ (0...(𝑁 − 1)) ↔ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))))
144143anbi2d 742 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))))
145 uncom 3900 . . . . . . . . . . . . . . . 16 ((0...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ (0...(𝑁 − 1)))
146145difeq1i 3867 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))) = (({𝑁} ∪ (0...(𝑁 − 1))) ∖ (0...(𝑁 − 1)))
147 difun2 4192 . . . . . . . . . . . . . . 15 (({𝑁} ∪ (0...(𝑁 − 1))) ∖ (0...(𝑁 − 1))) = ({𝑁} ∖ (0...(𝑁 − 1)))
148146, 147eqtri 2782 . . . . . . . . . . . . . 14 (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))) = ({𝑁} ∖ (0...(𝑁 − 1)))
1491nncnd 11248 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
150 npcan1 10667 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
151149, 150syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1521nnnn0d 11563 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
153152, 126syl6eleq 2849 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154151, 153eqeltrd 2839 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘0))
15512nn0zd 11692 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) ∈ ℤ)
156 uzid 11914 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
157 peano2uz 11954 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
158155, 156, 1573syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
159151, 158eqeltrrd 2840 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
160 fzsplit2 12579 . . . . . . . . . . . . . . . . 17 ((((𝑁 − 1) + 1) ∈ (ℤ‘0) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
161154, 159, 160syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
162151oveq1d 6829 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
1631nnzd 11693 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
164 fzsn 12596 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
165163, 164syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁...𝑁) = {𝑁})
166162, 165eqtrd 2794 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
167166uneq2d 3910 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((0...(𝑁 − 1)) ∪ {𝑁}))
168161, 167eqtrd 2794 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ {𝑁}))
169168difeq1d 3870 . . . . . . . . . . . . . 14 (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1))))
170 elfzle2 12558 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (0...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
17115, 170nsyl 135 . . . . . . . . . . . . . . 15 (𝜑 → ¬ 𝑁 ∈ (0...(𝑁 − 1)))
172 incom 3948 . . . . . . . . . . . . . . . . 17 ((0...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (0...(𝑁 − 1)))
173172eqeq1i 2765 . . . . . . . . . . . . . . . 16 (((0...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (0...(𝑁 − 1))) = ∅)
174 disjsn 4390 . . . . . . . . . . . . . . . 16 (((0...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (0...(𝑁 − 1)))
175 disj3 4164 . . . . . . . . . . . . . . . 16 (({𝑁} ∩ (0...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
176173, 174, 1753bitr3i 290 . . . . . . . . . . . . . . 15 𝑁 ∈ (0...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
177171, 176sylib 208 . . . . . . . . . . . . . 14 (𝜑 → {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1))))
178148, 169, 1773eqtr4a 2820 . . . . . . . . . . . . 13 (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = {𝑁})
179178eleq2d 2825 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑧) ∈ ((0...𝑁) ∖ (0...(𝑁 − 1))) ↔ (2nd𝑧) ∈ {𝑁}))
180 eldif 3725 . . . . . . . . . . . 12 ((2nd𝑧) ∈ ((0...𝑁) ∖ (0...(𝑁 − 1))) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))))
181138elsn 4336 . . . . . . . . . . . 12 ((2nd𝑧) ∈ {𝑁} ↔ (2nd𝑧) = 𝑁)
182179, 180, 1813bitr3g 302 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (0...(𝑁 − 1))) ↔ (2nd𝑧) = 𝑁))
183144, 182bitr3d 270 . . . . . . . . . 10 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))) ↔ (2nd𝑧) = 𝑁))
184183biimpd 219 . . . . . . . . 9 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))) → (2nd𝑧) = 𝑁))
185184expdimp 452 . . . . . . . 8 ((𝜑 ∧ (2nd𝑧) ∈ (0...𝑁)) → ((¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) = 𝑁))
186125, 185sylan2 492 . . . . . . 7 ((𝜑𝑧𝑆) → ((¬ (2nd𝑧) = 0 ∧ ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) = 𝑁))
187123, 186mpan2d 712 . . . . . 6 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 0 → (2nd𝑧) = 𝑁))
1881, 2, 3poimirlem14 33754 . . . . . . . . . 10 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
189 fveq2 6353 . . . . . . . . . . . 12 (𝑧 = 𝑠 → (2nd𝑧) = (2nd𝑠))
190189eqeq1d 2762 . . . . . . . . . . 11 (𝑧 = 𝑠 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑠) = 𝑁))
191190rmo4 3540 . . . . . . . . . 10 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
192188, 191sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
193192r19.21bi 3070 . . . . . . . 8 ((𝜑𝑧𝑆) → ∀𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠))
1944adantr 472 . . . . . . . 8 ((𝜑𝑧𝑆) → 𝑇𝑆)
195 fveq2 6353 . . . . . . . . . . . 12 (𝑠 = 𝑇 → (2nd𝑠) = (2nd𝑇))
196195eqeq1d 2762 . . . . . . . . . . 11 (𝑠 = 𝑇 → ((2nd𝑠) = 𝑁 ↔ (2nd𝑇) = 𝑁))
197196anbi2d 742 . . . . . . . . . 10 (𝑠 = 𝑇 → (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) ↔ ((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁)))
198 eqeq2 2771 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝑧 = 𝑠𝑧 = 𝑇))
199197, 198imbi12d 333 . . . . . . . . 9 (𝑠 = 𝑇 → ((((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠) ↔ (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇)))
200199rspccv 3446 . . . . . . . 8 (∀𝑠𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑠) = 𝑁) → 𝑧 = 𝑠) → (𝑇𝑆 → (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇)))
201193, 194, 200sylc 65 . . . . . . 7 ((𝜑𝑧𝑆) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑇) = 𝑁) → 𝑧 = 𝑇))
2028, 201mpan2d 712 . . . . . 6 ((𝜑𝑧𝑆) → ((2nd𝑧) = 𝑁𝑧 = 𝑇))
203187, 202syld 47 . . . . 5 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 0 → 𝑧 = 𝑇))
204203necon1ad 2949 . . . 4 ((𝜑𝑧𝑆) → (𝑧𝑇 → (2nd𝑧) = 0))
205204ralrimiva 3104 . . 3 (𝜑 → ∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 0))
2061, 2, 3poimirlem13 33753 . . 3 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 0)
207 rmoim 3548 . . 3 (∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 0) → (∃*𝑧𝑆 (2nd𝑧) = 0 → ∃*𝑧𝑆 𝑧𝑇))
208205, 206, 207sylc 65 . 2 (𝜑 → ∃*𝑧𝑆 𝑧𝑇)
209 reu5 3298 . 2 (∃!𝑧𝑆 𝑧𝑇 ↔ (∃𝑧𝑆 𝑧𝑇 ∧ ∃*𝑧𝑆 𝑧𝑇))
2107, 208, 209sylanbrc 701 1 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1632  wcel 2139  {cab 2746  wne 2932  wral 3050  wrex 3051  ∃!wreu 3052  ∃*wrmo 3053  {crab 3054  csb 3674  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058  ifcif 4230  {csn 4321   class class class wbr 4804  cmpt 4881   × cxp 5264  ran crn 5267  cima 5269  wf 6045  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6814  𝑓 cof 7061  1st c1st 7332  2nd c2nd 7333  𝑚 cmap 8025  cc 10146  0cc0 10148  1c1 10149   + caddc 10151   < clt 10286  cle 10287  cmin 10478  cn 11232  0cn0 11504  cz 11589  cuz 11899  ...cfz 12539  ..^cfzo 12679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-n0 11505  df-z 11590  df-uz 11900  df-fz 12540  df-fzo 12680
This theorem is referenced by:  poimirlem22  33762
  Copyright terms: Public domain W3C validator