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

Theorem poimirlem14 33756
Description: Lemma for poimir 33775- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (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...𝑁)))
Assertion
Ref Expression
poimirlem14 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
Distinct variable groups:   𝑓,𝑗,𝑡,𝑦,𝑧   𝜑,𝑗,𝑦   𝑗,𝐹,𝑦   𝑗,𝑁,𝑦   𝜑,𝑡   𝑓,𝐾,𝑗,𝑡   𝑓,𝑁,𝑡   𝜑,𝑧   𝑓,𝐹,𝑡,𝑧   𝑧,𝐾   𝑧,𝑁   𝑆,𝑗,𝑡,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem14
Dummy variables 𝑘 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
21ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑁 ∈ ℕ)
3 poimirlem22.s . . . . . . . 8 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4 simplrl 762 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧𝑆)
51nngt0d 11266 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
6 breq2 4790 . . . . . . . . . . 11 ((2nd𝑧) = 𝑁 → (0 < (2nd𝑧) ↔ 0 < 𝑁))
76biimparc 465 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
85, 7sylan 569 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
98ad2ant2r 741 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑧))
102, 3, 4, 9poimirlem5 33747 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑧)))
11 simplrr 763 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑘𝑆)
12 breq2 4790 . . . . . . . . . . 11 ((2nd𝑘) = 𝑁 → (0 < (2nd𝑘) ↔ 0 < 𝑁))
1312biimparc 465 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
145, 13sylan 569 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
1514ad2ant2rl 743 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑘))
162, 3, 11, 15poimirlem5 33747 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑘)))
1710, 16eqtr3d 2807 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑘)))
18 elrabi 3510 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑡 ∈ ((((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...𝑁)))
1918, 3eleq2s 2868 . . . . . . . . . . . 12 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
20 xp1st 7347 . . . . . . . . . . . 12 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
21 xp2nd 7348 . . . . . . . . . . . 12 ((1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
2219, 20, 213syl 18 . . . . . . . . . . 11 (𝑧𝑆 → (2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
23 fvex 6342 . . . . . . . . . . . 12 (2nd ‘(1st𝑧)) ∈ V
24 f1oeq1 6268 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
2523, 24elab 3501 . . . . . . . . . . 11 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
2622, 25sylib 208 . . . . . . . . . 10 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
27 f1ofn 6279 . . . . . . . . . 10 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2826, 27syl 17 . . . . . . . . 9 (𝑧𝑆 → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2928adantr 466 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
3029ad2antlr 706 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
31 elrabi 3510 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑡 ∈ ((((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 2868 . . . . . . . . . . . 12 (𝑘𝑆𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33 xp1st 7347 . . . . . . . . . . . 12 (𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp2nd 7348 . . . . . . . . . . . 12 ((1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
3532, 33, 343syl 18 . . . . . . . . . . 11 (𝑘𝑆 → (2nd ‘(1st𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
36 fvex 6342 . . . . . . . . . . . 12 (2nd ‘(1st𝑘)) ∈ V
37 f1oeq1 6268 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
3836, 37elab 3501 . . . . . . . . . . 11 ((2nd ‘(1st𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
3935, 38sylib 208 . . . . . . . . . 10 (𝑘𝑆 → (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
40 f1ofn 6279 . . . . . . . . . 10 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4139, 40syl 17 . . . . . . . . 9 (𝑘𝑆 → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4241adantl 467 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4342ad2antlr 706 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
44 simpllr 760 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧𝑆𝑘𝑆))
45 oveq2 6801 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
4645imaeq2d 5607 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
47 f1ofo 6285 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
48 foima 6261 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
4926, 47, 483syl 18 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
5046, 49sylan9eqr 2827 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5150adantlr 694 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5245imaeq2d 5607 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑁)))
53 f1ofo 6285 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁))
54 foima 6261 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5539, 53, 543syl 18 . . . . . . . . . . . . . . 15 (𝑘𝑆 → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5652, 55sylan9eqr 2827 . . . . . . . . . . . . . 14 ((𝑘𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5756adantll 693 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5851, 57eqtr4d 2808 . . . . . . . . . . . 12 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
5944, 58sylan 569 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
60 simpll 750 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝜑)
61 elnnuz 11926 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
621, 61sylib 208 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
63 fzm1 12627 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6564anbi1d 615 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁)))
6665biimpa 462 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁))
67 df-ne 2944 . . . . . . . . . . . . . . . . . 18 (𝑛𝑁 ↔ ¬ 𝑛 = 𝑁)
6867anbi2i 609 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁))
69 pm5.61 985 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7068, 69bitri 264 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7166, 70sylib 208 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
72 fz1ssfz0 12643 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
7372sseli 3748 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ (0...(𝑁 − 1)))
7473adantr 466 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁) → 𝑛 ∈ (0...(𝑁 − 1)))
7571, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
7660, 75sylan 569 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
77 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1))))
7877anbi2d 614 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1)))))
79 oveq2 6801 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
8079imaeq2d 5607 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...𝑛)))
8179imaeq2d 5607 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
8280, 81eqeq12d 2786 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛))))
8378, 82imbi12d 333 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚))) ↔ ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))))
841ad3antrrr 709 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
85 poimirlem22.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
8685ad3antrrr 709 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
87 simpl 468 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑧𝑆)
8887ad3antlr 710 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧𝑆)
89 simplrl 762 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑧) = 𝑁)
90 simpr 471 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑘𝑆)
9190ad3antlr 710 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘𝑆)
92 simplrr 763 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑘) = 𝑁)
93 simpr 471 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1)))
9484, 3, 86, 88, 89, 91, 92, 93poimirlem12 33754 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9584, 3, 86, 91, 92, 88, 89, 93poimirlem12 33754 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑧)) “ (1...𝑚)))
9694, 95eqssd 3769 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9783, 96chvarv 2425 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9876, 97syldan 579 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9998anassrs 458 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
10059, 99pm2.61dane 3030 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
101 simpr 471 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
102 elfzelz 12549 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1031nnzd 11683 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
104 elfzm1b 12625 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
105102, 103, 104syl2anr 584 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
106101, 105mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
10760, 106sylan 569 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
108 ovex 6823 . . . . . . . . . . . 12 (𝑛 − 1) ∈ V
109 eleq1 2838 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
110109anbi2d 614 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
111 oveq2 6801 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1)))
112111imaeq2d 5607 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))
113111imaeq2d 5607 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
114112, 113eqeq12d 2786 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
115110, 114imbi12d 333 . . . . . . . . . . . 12 (𝑚 = (𝑛 − 1) → (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚))) ↔ ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))))
116108, 115, 96vtocl 3410 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
117107, 116syldan 579 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
118100, 117difeq12d 3880 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
119 fnsnfv 6400 . . . . . . . . . . . 12 (((2nd ‘(1st𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
12028, 119sylan 569 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
121 elfznn 12577 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
122 uncom 3908 . . . . . . . . . . . . . . . . 17 ((1...(𝑛 − 1)) ∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1)))
123122difeq1i 3875 . . . . . . . . . . . . . . . 16 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1)))
124 difun2 4190 . . . . . . . . . . . . . . . 16 (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
125123, 124eqtri 2793 . . . . . . . . . . . . . . 15 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
126 nncn 11230 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
127 npcan1 10657 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
128126, 127syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛)
129 elnnuz 11926 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
130129biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
131128, 130eqeltrd 2850 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
132 nnm1nn0 11536 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
133132nn0zd 11682 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℤ)
134 uzid 11903 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
135 peano2uz 11943 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
136133, 134, 1353syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
137128, 136eqeltrrd 2851 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
138 fzsplit2 12573 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
139131, 137, 138syl2anc 573 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
140128oveq1d 6808 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
141 nnz 11601 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
142 fzsn 12590 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛})
144140, 143eqtrd 2805 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
145144uneq2d 3918 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
146139, 145eqtrd 2805 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
147146difeq1d 3878 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))))
148 nnre 11229 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
149 ltm1 11065 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
150 peano2rem 10550 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
151 ltnle 10319 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
152150, 151mpancom 668 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
153149, 152mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
154 elfzle2 12552 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1))
155153, 154nsyl 137 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
156148, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
157 incom 3956 . . . . . . . . . . . . . . . . . 18 ((1...(𝑛 − 1)) ∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1)))
158157eqeq1i 2776 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ({𝑛} ∩ (1...(𝑛 − 1))) = ∅)
159 disjsn 4383 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ (1...(𝑛 − 1)))
160 disj3 4164 . . . . . . . . . . . . . . . . 17 (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
161158, 159, 1603bitr3i 290 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
162156, 161sylib 208 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
163125, 147, 1623eqtr4a 2831 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
164121, 163syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
165164imaeq2d 5607 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
166165adantl 467 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
167 dff1o3 6284 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑧))))
168167simprbi 484 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑧)))
169 imadif 6113 . . . . . . . . . . . . 13 (Fun (2nd ‘(1st𝑧)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
17026, 168, 1693syl 18 . . . . . . . . . . . 12 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
171170adantr 466 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
172120, 166, 1713eqtr2d 2811 . . . . . . . . . 10 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
1734, 172sylan 569 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
174 eleq1 2838 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (𝑧𝑆𝑘𝑆))
175174anbi1d 615 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ((𝑧𝑆𝑛 ∈ (1...𝑁)) ↔ (𝑘𝑆𝑛 ∈ (1...𝑁))))
176 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑘 → (1st𝑧) = (1st𝑘))
177176fveq2d 6336 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
178177fveq1d 6334 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
179178sneqd 4328 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
180177imaeq1d 5606 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
181177imaeq1d 5606 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
182180, 181difeq12d 3880 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
183179, 182eqeq12d 2786 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ({((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))))
184175, 183imbi12d 333 . . . . . . . . . . 11 (𝑧 = 𝑘 → (((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))))
185184, 172chvarv 2425 . . . . . . . . . 10 ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
18611, 185sylan 569 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
187118, 173, 1863eqtr4d 2815 . . . . . . . 8 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
188 fvex 6342 . . . . . . . . 9 ((2nd ‘(1st𝑧))‘𝑛) ∈ V
189188sneqr 4504 . . . . . . . 8 ({((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)} → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
190187, 189syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
19130, 43, 190eqfnfvd 6457 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
19219, 20syl 17 . . . . . . . 8 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
19332, 33syl 17 . . . . . . . 8 (𝑘𝑆 → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
194 xpopth 7356 . . . . . . . 8 (((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𝑘)))
195192, 193, 194syl2an 583 . . . . . . 7 ((𝑧𝑆𝑘𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
196195ad2antlr 706 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
19717, 191, 196mpbi2and 691 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st𝑧) = (1st𝑘))
198 eqtr3 2792 . . . . . 6 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → (2nd𝑧) = (2nd𝑘))
199198adantl 467 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd𝑧) = (2nd𝑘))
200 xpopth 7356 . . . . . . 7 ((𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
20119, 32, 200syl2an 583 . . . . . 6 ((𝑧𝑆𝑘𝑆) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
202201ad2antlr 706 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
203197, 199, 202mpbi2and 691 . . . 4 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧 = 𝑘)
204203ex 397 . . 3 ((𝜑 ∧ (𝑧𝑆𝑘𝑆)) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
205204ralrimivva 3120 . 2 (𝜑 → ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
206 fveq2 6332 . . . 4 (𝑧 = 𝑘 → (2nd𝑧) = (2nd𝑘))
207206eqeq1d 2773 . . 3 (𝑧 = 𝑘 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑘) = 𝑁))
208207rmo4 3551 . 2 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
209205, 208sylibr 224 1 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wcel 2145  {cab 2757  wne 2943  wral 3061  ∃*wrmo 3064  {crab 3065  csb 3682  cdif 3720  cun 3721  cin 3722  c0 4063  ifcif 4225  {csn 4316   class class class wbr 4786  cmpt 4863   × cxp 5247  ccnv 5248  cima 5252  Fun wfun 6025   Fn wfn 6026  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  𝑓 cof 7042  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   < clt 10276  cle 10277  cmin 10468  cn 11222  cz 11579  cuz 11888  ...cfz 12533  ..^cfzo 12673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534  df-fzo 12674
This theorem is referenced by:  poimirlem18  33760  poimirlem21  33763
  Copyright terms: Public domain W3C validator