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

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

Proof of Theorem poimirlem18
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 poimirlem18.3 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
6 poimirlem18.4 . . 3 (𝜑 → (2nd𝑇) = 0)
71, 2, 3, 4, 5, 6poimirlem17 32596 . 2 (𝜑 → ∃𝑧𝑆 𝑧𝑇)
86adantr 480 . . . . . . . 8 ((𝜑𝑧𝑆) → (2nd𝑇) = 0)
9 0nnn 10929 . . . . . . . . . . . . 13 ¬ 0 ∈ ℕ
10 elfznn 12241 . . . . . . . . . . . . 13 (0 ∈ (1...(𝑁 − 1)) → 0 ∈ ℕ)
119, 10mto 187 . . . . . . . . . . . 12 ¬ 0 ∈ (1...(𝑁 − 1))
12 eleq1 2676 . . . . . . . . . . . 12 ((2nd𝑧) = 0 → ((2nd𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1))))
1311, 12mtbiri 316 . . . . . . . . . . 11 ((2nd𝑧) = 0 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))
1413necon2ai 2811 . . . . . . . . . 10 ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑧) ≠ 0)
151ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
16 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (2nd𝑡) = (2nd𝑧))
1716breq2d 4595 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑧)))
1817ifbid 4058 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)))
1918csbeq1d 3506 . . . . . . . . . . . . . . . . . . . 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}))))
20 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (1st𝑡) = (1st𝑧))
2120fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑧)))
2220fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑧 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑧)))
2322imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑧)) “ (1...𝑗)))
2423xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}))
2522imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑧 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)))
2625xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑧 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
2724, 26uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = 𝑧 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
2821, 27oveq12d 6567 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑧 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
2928csbeq2dv 3944 . . . . . . . . . . . . . . . . . . . 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}))))
3019, 29eqtrd 2644 . . . . . . . . . . . . . . . . . . 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}))))
3130mpteq2dv 4673 . . . . . . . . . . . . . . . . . 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})))))
3231eqeq2d 2620 . . . . . . . . . . . . . . . . 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}))))))
3332, 2elrab2 3333 . . . . . . . . . . . . . . . 16 (𝑧𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
3433simprbi 479 . . . . . . . . . . . . . . 15 (𝑧𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
3534ad2antlr 759 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑧), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑧)) ∘𝑓 + ((((2nd ‘(1st𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
36 elrabi 3328 . . . . . . . . . . . . . . . . . . . 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...𝑁)))
3736, 2eleq2s 2706 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
38 xp1st 7089 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3937, 38syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
40 xp1st 7089 . . . . . . . . . . . . . . . . . 18 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
4139, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 → (1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
42 elmapi 7765 . . . . . . . . . . . . . . . . 17 ((1st ‘(1st𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
4341, 42syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾))
44 elfzoelz 12339 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
4544ssriv 3572 . . . . . . . . . . . . . . . 16 (0..^𝐾) ⊆ ℤ
46 fss 5969 . . . . . . . . . . . . . . . 16 (((1st ‘(1st𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
4743, 45, 46sylancl 693 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
4847ad2antlr 759 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (1st ‘(1st𝑧)):(1...𝑁)⟶ℤ)
49 xp2nd 7090 . . . . . . . . . . . . . . . . 17 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5039, 49syl 17 . . . . . . . . . . . . . . . 16 (𝑧𝑆 → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
51 fvex 6113 . . . . . . . . . . . . . . . . 17 (2nd ‘(1st𝑧)) ∈ V
52 f1oeq1 6040 . . . . . . . . . . . . . . . . 17 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
5351, 52elab 3319 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
5450, 53sylib 207 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
5554ad2antlr 759 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
56 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
5715, 35, 48, 55, 56poimirlem1 32580 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
581ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝑁 ∈ ℕ)
59 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
6059breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
6160ifbid 4058 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
6261csbeq1d 3506 . . . . . . . . . . . . . . . . . . . . . . . 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}))))
63 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
6463fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
6563fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
6665imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
6766xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
6865imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
6968xpeq1d 5062 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
7067, 69uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
7164, 70oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
7271csbeq2dv 3944 . . . . . . . . . . . . . . . . . . . . . . . 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}))))
7362, 72eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 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}))))
7473mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . 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})))))
7574eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . 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}))))))
7675, 2elrab2 3333 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
7776simprbi 479 . . . . . . . . . . . . . . . . . . 19 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
784, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
7978ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
80 elrabi 3328 . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁)))
8180, 2eleq2s 2706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
824, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
83 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
85 xp1st 7089 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
87 elmapi 7765 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
8886, 87syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
89 fss 5969 . . . . . . . . . . . . . . . . . . 19 (((1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9088, 45, 89sylancl 693 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
9190ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (1st ‘(1st𝑇)):(1...𝑁)⟶ℤ)
92 xp2nd 7090 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
9384, 92syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
94 fvex 6113 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
95 f1oeq1 6040 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
9694, 95elab 3319 . . . . . . . . . . . . . . . . . . 19 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
9793, 96sylib 207 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
9897ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
99 simplr 788 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑧) ∈ (1...(𝑁 − 1)))
100 xp2nd 7090 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑇) ∈ (0...𝑁))
10182, 100syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
102101adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) ∈ (0...𝑁))
103 eldifsn 4260 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}) ↔ ((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)))
104103biimpri 217 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ (0...𝑁) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
105102, 104sylan 487 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → (2nd𝑇) ∈ ((0...𝑁) ∖ {(2nd𝑧)}))
10658, 79, 91, 98, 99, 105poimirlem2 32581 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd𝑇) ≠ (2nd𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛))
107106ex 449 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ (2nd𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛)))
108107necon1bd 2800 . . . . . . . . . . . . . 14 ((𝜑 ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
109108adantlr 747 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd𝑧))‘𝑛) → (2nd𝑇) = (2nd𝑧)))
11057, 109mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → (2nd𝑇) = (2nd𝑧))
111110neeq1d 2841 . . . . . . . . . . 11 (((𝜑𝑧𝑆) ∧ (2nd𝑧) ∈ (1...(𝑁 − 1))) → ((2nd𝑇) ≠ 0 ↔ (2nd𝑧) ≠ 0))
112111exbiri 650 . . . . . . . . . 10 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → ((2nd𝑧) ≠ 0 → (2nd𝑇) ≠ 0)))
11314, 112mpdi 44 . . . . . . . . 9 ((𝜑𝑧𝑆) → ((2nd𝑧) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≠ 0))
114113necon2bd 2798 . . . . . . . 8 ((𝜑𝑧𝑆) → ((2nd𝑇) = 0 → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1))))
1158, 114mpd 15 . . . . . . 7 ((𝜑𝑧𝑆) → ¬ (2nd𝑧) ∈ (1...(𝑁 − 1)))
116 xp2nd 7090 . . . . . . . . 9 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd𝑧) ∈ (0...𝑁))
11737, 116syl 17 . . . . . . . 8 (𝑧𝑆 → (2nd𝑧) ∈ (0...𝑁))
1181nncnd 10913 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
119 npcan1 10334 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
120118, 119syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
121 nnuz 11599 . . . . . . . . . . . . . . . . . . 19 ℕ = (ℤ‘1)
1221, 121syl6eleq 2698 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘1))
123120, 122eqeltrd 2688 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
1241nnzd 11357 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
125 peano2zm 11297 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
126124, 125syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) ∈ ℤ)
127 uzid 11578 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
128 peano2uz 11617 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
129126, 127, 1283syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
130120, 129eqeltrrd 2689 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
131 fzsplit2 12237 . . . . . . . . . . . . . . . . 17 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
132123, 130, 131syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
133120oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
134 fzsn 12254 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
135124, 134syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁...𝑁) = {𝑁})
136133, 135eqtrd 2644 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
137136uneq2d 3729 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
138132, 137eqtrd 2644 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
139138eleq2d 2673 . . . . . . . . . . . . . 14 (𝜑 → ((2nd𝑧) ∈ (1...𝑁) ↔ (2nd𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
140139notbid 307 . . . . . . . . . . . . 13 (𝜑 → (¬ (2nd𝑧) ∈ (1...𝑁) ↔ ¬ (2nd𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
141 ioran 510 . . . . . . . . . . . . . 14 (¬ ((2nd𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd𝑧) = 𝑁) ↔ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁))
142 elun 3715 . . . . . . . . . . . . . . 15 ((2nd𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd𝑧) ∈ {𝑁}))
143 fvex 6113 . . . . . . . . . . . . . . . . 17 (2nd𝑧) ∈ V
144143elsn 4140 . . . . . . . . . . . . . . . 16 ((2nd𝑧) ∈ {𝑁} ↔ (2nd𝑧) = 𝑁)
145144orbi2i 540 . . . . . . . . . . . . . . 15 (((2nd𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd𝑧) ∈ {𝑁}) ↔ ((2nd𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd𝑧) = 𝑁))
146142, 145bitri 263 . . . . . . . . . . . . . 14 ((2nd𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd𝑧) = 𝑁))
147141, 146xchnxbir 322 . . . . . . . . . . . . 13 (¬ (2nd𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁))
148140, 147syl6bb 275 . . . . . . . . . . . 12 (𝜑 → (¬ (2nd𝑧) ∈ (1...𝑁) ↔ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁)))
149148anbi2d 736 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (1...𝑁)) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁))))
1501nnnn0d 11228 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
151 nn0uz 11598 . . . . . . . . . . . . . . . . 17 0 = (ℤ‘0)
152150, 151syl6eleq 2698 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ‘0))
153 fzpred 12259 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
154152, 153syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
155154difeq1d 3689 . . . . . . . . . . . . . 14 (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)))
156 difun2 4000 . . . . . . . . . . . . . . 15 (({0} ∪ (1...𝑁)) ∖ (1...𝑁)) = ({0} ∖ (1...𝑁))
157 0p1e1 11009 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
158157oveq1i 6559 . . . . . . . . . . . . . . . . 17 ((0 + 1)...𝑁) = (1...𝑁)
159158uneq2i 3726 . . . . . . . . . . . . . . . 16 ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
160159difeq1i 3686 . . . . . . . . . . . . . . 15 (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = (({0} ∪ (1...𝑁)) ∖ (1...𝑁))
161 incom 3767 . . . . . . . . . . . . . . . . 17 ({0} ∩ (1...𝑁)) = ((1...𝑁) ∩ {0})
162 elfznn 12241 . . . . . . . . . . . . . . . . . . 19 (0 ∈ (1...𝑁) → 0 ∈ ℕ)
1639, 162mto 187 . . . . . . . . . . . . . . . . . 18 ¬ 0 ∈ (1...𝑁)
164 disjsn 4192 . . . . . . . . . . . . . . . . . 18 (((1...𝑁) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...𝑁))
165163, 164mpbir 220 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∩ {0}) = ∅
166161, 165eqtri 2632 . . . . . . . . . . . . . . . 16 ({0} ∩ (1...𝑁)) = ∅
167 disj3 3973 . . . . . . . . . . . . . . . 16 (({0} ∩ (1...𝑁)) = ∅ ↔ {0} = ({0} ∖ (1...𝑁)))
168166, 167mpbi 219 . . . . . . . . . . . . . . 15 {0} = ({0} ∖ (1...𝑁))
169156, 160, 1683eqtr4i 2642 . . . . . . . . . . . . . 14 (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = {0}
170155, 169syl6eq 2660 . . . . . . . . . . . . 13 (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0})
171170eleq2d 2673 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ (2nd𝑧) ∈ {0}))
172 eldif 3550 . . . . . . . . . . . 12 ((2nd𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (1...𝑁)))
173143elsn 4140 . . . . . . . . . . . 12 ((2nd𝑧) ∈ {0} ↔ (2nd𝑧) = 0)
174171, 172, 1733bitr3g 301 . . . . . . . . . . 11 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ ¬ (2nd𝑧) ∈ (1...𝑁)) ↔ (2nd𝑧) = 0))
175149, 174bitr3d 269 . . . . . . . . . 10 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁)) ↔ (2nd𝑧) = 0))
176175biimpd 218 . . . . . . . . 9 (𝜑 → (((2nd𝑧) ∈ (0...𝑁) ∧ (¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁)) → (2nd𝑧) = 0))
177176expdimp 452 . . . . . . . 8 ((𝜑 ∧ (2nd𝑧) ∈ (0...𝑁)) → ((¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁) → (2nd𝑧) = 0))
178117, 177sylan2 490 . . . . . . 7 ((𝜑𝑧𝑆) → ((¬ (2nd𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd𝑧) = 𝑁) → (2nd𝑧) = 0))
179115, 178mpand 707 . . . . . 6 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 𝑁 → (2nd𝑧) = 0))
1801, 2, 3poimirlem13 32592 . . . . . . . . . 10 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 0)
181 fveq2 6103 . . . . . . . . . . . 12 (𝑧 = 𝑠 → (2nd𝑧) = (2nd𝑠))
182181eqeq1d 2612 . . . . . . . . . . 11 (𝑧 = 𝑠 → ((2nd𝑧) = 0 ↔ (2nd𝑠) = 0))
183182rmo4 3366 . . . . . . . . . 10 (∃*𝑧𝑆 (2nd𝑧) = 0 ↔ ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) → 𝑧 = 𝑠))
184180, 183sylib 207 . . . . . . . . 9 (𝜑 → ∀𝑧𝑆𝑠𝑆 (((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) → 𝑧 = 𝑠))
185184r19.21bi 2916 . . . . . . . 8 ((𝜑𝑧𝑆) → ∀𝑠𝑆 (((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) → 𝑧 = 𝑠))
1864adantr 480 . . . . . . . 8 ((𝜑𝑧𝑆) → 𝑇𝑆)
187 fveq2 6103 . . . . . . . . . . . 12 (𝑠 = 𝑇 → (2nd𝑠) = (2nd𝑇))
188187eqeq1d 2612 . . . . . . . . . . 11 (𝑠 = 𝑇 → ((2nd𝑠) = 0 ↔ (2nd𝑇) = 0))
189188anbi2d 736 . . . . . . . . . 10 (𝑠 = 𝑇 → (((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) ↔ ((2nd𝑧) = 0 ∧ (2nd𝑇) = 0)))
190 eqeq2 2621 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝑧 = 𝑠𝑧 = 𝑇))
191189, 190imbi12d 333 . . . . . . . . 9 (𝑠 = 𝑇 → ((((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2nd𝑧) = 0 ∧ (2nd𝑇) = 0) → 𝑧 = 𝑇)))
192191rspccv 3279 . . . . . . . 8 (∀𝑠𝑆 (((2nd𝑧) = 0 ∧ (2nd𝑠) = 0) → 𝑧 = 𝑠) → (𝑇𝑆 → (((2nd𝑧) = 0 ∧ (2nd𝑇) = 0) → 𝑧 = 𝑇)))
193185, 186, 192sylc 63 . . . . . . 7 ((𝜑𝑧𝑆) → (((2nd𝑧) = 0 ∧ (2nd𝑇) = 0) → 𝑧 = 𝑇))
1948, 193mpan2d 706 . . . . . 6 ((𝜑𝑧𝑆) → ((2nd𝑧) = 0 → 𝑧 = 𝑇))
195179, 194syld 46 . . . . 5 ((𝜑𝑧𝑆) → (¬ (2nd𝑧) = 𝑁𝑧 = 𝑇))
196195necon1ad 2799 . . . 4 ((𝜑𝑧𝑆) → (𝑧𝑇 → (2nd𝑧) = 𝑁))
197196ralrimiva 2949 . . 3 (𝜑 → ∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 𝑁))
1981, 2, 3poimirlem14 32593 . . 3 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
199 rmoim 3374 . . 3 (∀𝑧𝑆 (𝑧𝑇 → (2nd𝑧) = 𝑁) → (∃*𝑧𝑆 (2nd𝑧) = 𝑁 → ∃*𝑧𝑆 𝑧𝑇))
200197, 198, 199sylc 63 . 2 (𝜑 → ∃*𝑧𝑆 𝑧𝑇)
201 reu5 3136 . 2 (∃!𝑧𝑆 𝑧𝑇 ↔ (∃𝑧𝑆 𝑧𝑇 ∧ ∃*𝑧𝑆 𝑧𝑇))
2027, 200, 201sylanbrc 695 1 (𝜑 → ∃!𝑧𝑆 𝑧𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899  {crab 2900  ⦋csb 3499   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ran crn 5039   “ cima 5041  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  ℂcc 9813  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   − 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-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-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335 This theorem is referenced by:  poimirlem22  32601
 Copyright terms: Public domain W3C validator