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

Theorem poimirlem14 35222
 Description: Lemma for poimir 35241- 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..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (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 725 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑁 ∈ ℕ)
3 poimirlem22.s . . . . . . . 8 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4 simplrl 776 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧𝑆)
51nngt0d 11692 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
6 breq2 5038 . . . . . . . . . . 11 ((2nd𝑧) = 𝑁 → (0 < (2nd𝑧) ↔ 0 < 𝑁))
76biimparc 483 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
85, 7sylan 583 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
98ad2ant2r 746 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑧))
102, 3, 4, 9poimirlem5 35213 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑧)))
11 simplrr 777 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑘𝑆)
12 breq2 5038 . . . . . . . . . . 11 ((2nd𝑘) = 𝑁 → (0 < (2nd𝑘) ↔ 0 < 𝑁))
1312biimparc 483 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
145, 13sylan 583 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
1514ad2ant2rl 748 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑘))
162, 3, 11, 15poimirlem5 35213 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑘)))
1710, 16eqtr3d 2835 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑘)))
18 elrabi 3624 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
1918, 3eleq2s 2908 . . . . . . . . . . . 12 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
20 xp1st 7716 . . . . . . . . . . . 12 (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
21 xp2nd 7717 . . . . . . . . . . . 12 ((1st𝑧) ∈ (((0..^𝐾) ↑m (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 6668 . . . . . . . . . . . 12 (2nd ‘(1st𝑧)) ∈ V
24 f1oeq1 6587 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
2523, 24elab 3616 . . . . . . . . . . 11 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
2622, 25sylib 221 . . . . . . . . . 10 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
27 f1ofn 6600 . . . . . . . . . 10 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2826, 27syl 17 . . . . . . . . 9 (𝑧𝑆 → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2928adantr 484 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
3029ad2antlr 726 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
31 elrabi 3624 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3231, 3eleq2s 2908 . . . . . . . . . . . 12 (𝑘𝑆𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33 xp1st 7716 . . . . . . . . . . . 12 (𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp2nd 7717 . . . . . . . . . . . 12 ((1st𝑘) ∈ (((0..^𝐾) ↑m (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 6668 . . . . . . . . . . . 12 (2nd ‘(1st𝑘)) ∈ V
37 f1oeq1 6587 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
3836, 37elab 3616 . . . . . . . . . . 11 ((2nd ‘(1st𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
3935, 38sylib 221 . . . . . . . . . 10 (𝑘𝑆 → (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
40 f1ofn 6600 . . . . . . . . . 10 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4139, 40syl 17 . . . . . . . . 9 (𝑘𝑆 → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4241adantl 485 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4342ad2antlr 726 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
44 simpllr 775 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧𝑆𝑘𝑆))
45 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
4645imaeq2d 5900 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
47 f1ofo 6606 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
48 foima 6578 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
4926, 47, 483syl 18 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
5046, 49sylan9eqr 2855 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5150adantlr 714 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5245imaeq2d 5900 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑁)))
53 f1ofo 6606 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁))
54 foima 6578 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5539, 53, 543syl 18 . . . . . . . . . . . . . . 15 (𝑘𝑆 → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5652, 55sylan9eqr 2855 . . . . . . . . . . . . . 14 ((𝑘𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5756adantll 713 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5851, 57eqtr4d 2836 . . . . . . . . . . . 12 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
5944, 58sylan 583 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
60 simpll 766 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝜑)
61 elnnuz 12290 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
621, 61sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
63 fzm1 13002 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6564anbi1d 632 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁)))
6665biimpa 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁))
67 df-ne 2988 . . . . . . . . . . . . . . . . . 18 (𝑛𝑁 ↔ ¬ 𝑛 = 𝑁)
6867anbi2i 625 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁))
69 pm5.61 998 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7068, 69bitri 278 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7166, 70sylib 221 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
72 fz1ssfz0 13018 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
7372sseli 3913 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ (0...(𝑁 − 1)))
7473adantr 484 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁) → 𝑛 ∈ (0...(𝑁 − 1)))
7571, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
7660, 75sylan 583 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
77 eleq1 2877 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1))))
7877anbi2d 631 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1)))))
79 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
8079imaeq2d 5900 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...𝑛)))
8179imaeq2d 5900 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
8280, 81eqeq12d 2814 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛))))
8378, 82imbi12d 348 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚))) ↔ ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))))
841ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
85 poimirlem22.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
8685ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
87 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑧𝑆)
8887ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧𝑆)
89 simplrl 776 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑧) = 𝑁)
90 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑘𝑆)
9190ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘𝑆)
92 simplrr 777 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑘) = 𝑁)
93 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1)))
9484, 3, 86, 88, 89, 91, 92, 93poimirlem12 35220 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9584, 3, 86, 91, 92, 88, 89, 93poimirlem12 35220 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑧)) “ (1...𝑚)))
9694, 95eqssd 3934 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9783, 96chvarvv 2005 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9876, 97syldan 594 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9998anassrs 471 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
10059, 99pm2.61dane 3074 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
101 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
102 elfzelz 12922 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1031nnzd 12094 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
104 elfzm1b 13000 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
105102, 103, 104syl2anr 599 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
106101, 105mpbid 235 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
10760, 106sylan 583 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
108 ovex 7178 . . . . . . . . . . . 12 (𝑛 − 1) ∈ V
109 eleq1 2877 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
110109anbi2d 631 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
111 oveq2 7153 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1)))
112111imaeq2d 5900 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))
113111imaeq2d 5900 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
114112, 113eqeq12d 2814 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
115110, 114imbi12d 348 . . . . . . . . . . . 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 3508 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
117107, 116syldan 594 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
118100, 117difeq12d 4054 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
119 fnsnfv 6728 . . . . . . . . . . . 12 (((2nd ‘(1st𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
12028, 119sylan 583 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
121 elfznn 12951 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
122 uncom 4083 . . . . . . . . . . . . . . . . 17 ((1...(𝑛 − 1)) ∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1)))
123122difeq1i 4049 . . . . . . . . . . . . . . . 16 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1)))
124 difun2 4390 . . . . . . . . . . . . . . . 16 (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
125123, 124eqtri 2821 . . . . . . . . . . . . . . 15 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
126 nncn 11651 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
127 npcan1 11072 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
128126, 127syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛)
129 elnnuz 12290 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
130129biimpi 219 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
131128, 130eqeltrd 2890 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
132 nnm1nn0 11944 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
133132nn0zd 12093 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℤ)
134 uzid 12266 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
135 peano2uz 12309 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
136133, 134, 1353syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
137128, 136eqeltrrd 2891 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
138 fzsplit2 12947 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
139131, 137, 138syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
140128oveq1d 7160 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
141 nnz 12012 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
142 fzsn 12964 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛})
144140, 143eqtrd 2833 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
145144uneq2d 4093 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
146139, 145eqtrd 2833 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
147146difeq1d 4052 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))))
148 nnre 11650 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
149 ltm1 11489 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
150 peano2rem 10960 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
151 ltnle 10727 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
152150, 151mpancom 687 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
153149, 152mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
154 elfzle2 12926 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1))
155153, 154nsyl 142 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
156148, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
157 incom 4131 . . . . . . . . . . . . . . . . . 18 ((1...(𝑛 − 1)) ∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1)))
158157eqeq1i 2803 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ({𝑛} ∩ (1...(𝑛 − 1))) = ∅)
159 disjsn 4610 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ (1...(𝑛 − 1)))
160 disj3 4364 . . . . . . . . . . . . . . . . 17 (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
161158, 159, 1603bitr3i 304 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
162156, 161sylib 221 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
163125, 147, 1623eqtr4a 2859 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
164121, 163syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
165164imaeq2d 5900 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
166165adantl 485 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
167 dff1o3 6605 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑧))))
168167simprbi 500 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑧)))
169 imadif 6416 . . . . . . . . . . . . 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 484 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
172120, 166, 1713eqtr2d 2839 . . . . . . . . . 10 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
1734, 172sylan 583 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
174 eleq1 2877 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (𝑧𝑆𝑘𝑆))
175174anbi1d 632 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ((𝑧𝑆𝑛 ∈ (1...𝑁)) ↔ (𝑘𝑆𝑛 ∈ (1...𝑁))))
176 2fveq3 6660 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
177176fveq1d 6657 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
178177sneqd 4540 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
179176imaeq1d 5899 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
180176imaeq1d 5899 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
181179, 180difeq12d 4054 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
182178, 181eqeq12d 2814 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ({((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))))
183175, 182imbi12d 348 . . . . . . . . . . 11 (𝑧 = 𝑘 → (((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))))
184183, 172chvarvv 2005 . . . . . . . . . 10 ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
18511, 184sylan 583 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
186118, 173, 1853eqtr4d 2843 . . . . . . . 8 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
187 fvex 6668 . . . . . . . . 9 ((2nd ‘(1st𝑧))‘𝑛) ∈ V
188187sneqr 4734 . . . . . . . 8 ({((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)} → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
189186, 188syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
19030, 43, 189eqfnfvd 6792 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
19119, 20syl 17 . . . . . . . 8 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
19232, 33syl 17 . . . . . . . 8 (𝑘𝑆 → (1st𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
193 xpopth 7725 . . . . . . . 8 (((1st𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1st𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
194191, 192, 193syl2an 598 . . . . . . 7 ((𝑧𝑆𝑘𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
195194ad2antlr 726 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
19617, 190, 195mpbi2and 711 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st𝑧) = (1st𝑘))
197 eqtr3 2820 . . . . . 6 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → (2nd𝑧) = (2nd𝑘))
198197adantl 485 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd𝑧) = (2nd𝑘))
199 xpopth 7725 . . . . . . 7 ((𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
20019, 32, 199syl2an 598 . . . . . 6 ((𝑧𝑆𝑘𝑆) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
201200ad2antlr 726 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
202196, 198, 201mpbi2and 711 . . . 4 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧 = 𝑘)
203202ex 416 . . 3 ((𝜑 ∧ (𝑧𝑆𝑘𝑆)) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
204203ralrimivva 3156 . 2 (𝜑 → ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
205 fveqeq2 6664 . . 3 (𝑧 = 𝑘 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑘) = 𝑁))
206205rmo4 3671 . 2 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
207204, 206sylibr 237 1 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃*wrmo 3109  {crab 3110  ⦋csb 3830   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882  ∅c0 4246  ifcif 4428  {csn 4528   class class class wbr 5034   ↦ cmpt 5114   × cxp 5521  ◡ccnv 5522   “ cima 5526  Fun wfun 6326   Fn wfn 6327  ⟶wf 6328  –onto→wfo 6330  –1-1-onto→wf1o 6331  ‘cfv 6332  (class class class)co 7145   ∘f cof 7398  1st c1st 7682  2nd c2nd 7683   ↑m cmap 8407  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545   + caddc 10547   < clt 10682   ≤ cle 10683   − cmin 10877  ℕcn 11643  ℤcz 11989  ℤ≥cuz 12251  ...cfz 12905  ..^cfzo 13048 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-er 8290  df-map 8409  df-en 8511  df-dom 8512  df-sdom 8513  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-nn 11644  df-n0 11904  df-z 11990  df-uz 12252  df-fz 12906  df-fzo 13049 This theorem is referenced by:  poimirlem18  35226  poimirlem21  35229
 Copyright terms: Public domain W3C validator