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 35528
Description: Lemma for poimir 35547- 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 726 . . . . . . . 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 777 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧𝑆)
51nngt0d 11879 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
6 breq2 5057 . . . . . . . . . . 11 ((2nd𝑧) = 𝑁 → (0 < (2nd𝑧) ↔ 0 < 𝑁))
76biimparc 483 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
85, 7sylan 583 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
98ad2ant2r 747 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑧))
102, 3, 4, 9poimirlem5 35519 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑧)))
11 simplrr 778 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑘𝑆)
12 breq2 5057 . . . . . . . . . . 11 ((2nd𝑘) = 𝑁 → (0 < (2nd𝑘) ↔ 0 < 𝑁))
1312biimparc 483 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
145, 13sylan 583 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
1514ad2ant2rl 749 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑘))
162, 3, 11, 15poimirlem5 35519 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑘)))
1710, 16eqtr3d 2779 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑘)))
18 elrabi 3596 . . . . . . . . . . . . 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 2856 . . . . . . . . . . . 12 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
20 xp1st 7793 . . . . . . . . . . . 12 (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
21 xp2nd 7794 . . . . . . . . . . . 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 6730 . . . . . . . . . . . 12 (2nd ‘(1st𝑧)) ∈ V
24 f1oeq1 6649 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
2523, 24elab 3587 . . . . . . . . . . 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 6662 . . . . . . . . . 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 727 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
31 elrabi 3596 . . . . . . . . . . . . 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 2856 . . . . . . . . . . . 12 (𝑘𝑆𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33 xp1st 7793 . . . . . . . . . . . 12 (𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp2nd 7794 . . . . . . . . . . . 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 6730 . . . . . . . . . . . 12 (2nd ‘(1st𝑘)) ∈ V
37 f1oeq1 6649 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
3836, 37elab 3587 . . . . . . . . . . 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 6662 . . . . . . . . . 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 727 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
44 simpllr 776 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧𝑆𝑘𝑆))
45 oveq2 7221 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
4645imaeq2d 5929 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
47 f1ofo 6668 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
48 foima 6638 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
4926, 47, 483syl 18 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
5046, 49sylan9eqr 2800 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5150adantlr 715 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5245imaeq2d 5929 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑁)))
53 f1ofo 6668 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁))
54 foima 6638 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5539, 53, 543syl 18 . . . . . . . . . . . . . . 15 (𝑘𝑆 → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5652, 55sylan9eqr 2800 . . . . . . . . . . . . . 14 ((𝑘𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5756adantll 714 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5851, 57eqtr4d 2780 . . . . . . . . . . . 12 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
5944, 58sylan 583 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
60 simpll 767 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝜑)
61 elnnuz 12478 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
621, 61sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
63 fzm1 13192 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6564anbi1d 633 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁)))
6665biimpa 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁))
67 df-ne 2941 . . . . . . . . . . . . . . . . . 18 (𝑛𝑁 ↔ ¬ 𝑛 = 𝑁)
6867anbi2i 626 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁))
69 pm5.61 1001 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7068, 69bitri 278 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7166, 70sylib 221 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
72 fz1ssfz0 13208 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
7372sseli 3896 . . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1))))
7877anbi2d 632 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1)))))
79 oveq2 7221 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
8079imaeq2d 5929 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...𝑛)))
8179imaeq2d 5929 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
8280, 81eqeq12d 2753 . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
85 poimirlem22.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
8685ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
87 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑧𝑆)
8887ad3antlr 731 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧𝑆)
89 simplrl 777 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑧) = 𝑁)
90 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑘𝑆)
9190ad3antlr 731 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘𝑆)
92 simplrr 778 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑘) = 𝑁)
93 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1)))
9484, 3, 86, 88, 89, 91, 92, 93poimirlem12 35526 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9584, 3, 86, 91, 92, 88, 89, 93poimirlem12 35526 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑧)) “ (1...𝑚)))
9694, 95eqssd 3918 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9783, 96chvarvv 2007 . . . . . . . . . . . . 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 3029 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
101 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
102 elfzelz 13112 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1031nnzd 12281 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
104 elfzm1b 13190 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
105102, 103, 104syl2anr 600 . . . . . . . . . . . . 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 7246 . . . . . . . . . . . 12 (𝑛 − 1) ∈ V
109 eleq1 2825 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
110109anbi2d 632 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
111 oveq2 7221 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1)))
112111imaeq2d 5929 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))
113111imaeq2d 5929 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
114112, 113eqeq12d 2753 . . . . . . . . . . . . 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 3474 . . . . . . . . . . 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 4038 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
119 fnsnfv 6790 . . . . . . . . . . . 12 (((2nd ‘(1st𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
12028, 119sylan 583 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
121 elfznn 13141 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
122 uncom 4067 . . . . . . . . . . . . . . . . 17 ((1...(𝑛 − 1)) ∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1)))
123122difeq1i 4033 . . . . . . . . . . . . . . . 16 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1)))
124 difun2 4395 . . . . . . . . . . . . . . . 16 (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
125123, 124eqtri 2765 . . . . . . . . . . . . . . 15 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
126 nncn 11838 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
127 npcan1 11257 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
128126, 127syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛)
129 elnnuz 12478 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
130129biimpi 219 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
131128, 130eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
132 nnm1nn0 12131 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
133132nn0zd 12280 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℤ)
134 uzid 12453 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
135 peano2uz 12497 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
136133, 134, 1353syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
137128, 136eqeltrrd 2839 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
138 fzsplit2 13137 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
139131, 137, 138syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
140128oveq1d 7228 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
141 nnz 12199 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
142 fzsn 13154 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛})
144140, 143eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
145144uneq2d 4077 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
146139, 145eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
147146difeq1d 4036 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))))
148 nnre 11837 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
149 ltm1 11674 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
150 peano2rem 11145 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
151 ltnle 10912 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
152150, 151mpancom 688 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
153149, 152mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
154 elfzle2 13116 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1))
155153, 154nsyl 142 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
156148, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
157 incom 4115 . . . . . . . . . . . . . . . . . 18 ((1...(𝑛 − 1)) ∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1)))
158157eqeq1i 2742 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ({𝑛} ∩ (1...(𝑛 − 1))) = ∅)
159 disjsn 4627 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ (1...(𝑛 − 1)))
160 disj3 4368 . . . . . . . . . . . . . . . . 17 (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
161158, 159, 1603bitr3i 304 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
162156, 161sylib 221 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
163125, 147, 1623eqtr4a 2804 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
164121, 163syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
165164imaeq2d 5929 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
166165adantl 485 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
167 dff1o3 6667 . . . . . . . . . . . . . 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 6464 . . . . . . . . . . . . 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 2783 . . . . . . . . . 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 2825 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (𝑧𝑆𝑘𝑆))
175174anbi1d 633 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ((𝑧𝑆𝑛 ∈ (1...𝑁)) ↔ (𝑘𝑆𝑛 ∈ (1...𝑁))))
176 2fveq3 6722 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
177176fveq1d 6719 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
178177sneqd 4553 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
179176imaeq1d 5928 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
180176imaeq1d 5928 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
181179, 180difeq12d 4038 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
182178, 181eqeq12d 2753 . . . . . . . . . . . 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 2007 . . . . . . . . . 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 2787 . . . . . . . 8 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
187 fvex 6730 . . . . . . . . 9 ((2nd ‘(1st𝑧))‘𝑛) ∈ V
188187sneqr 4751 . . . . . . . 8 ({((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)} → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
189186, 188syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
19030, 43, 189eqfnfvd 6855 . . . . . 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 7802 . . . . . . . 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 599 . . . . . . 7 ((𝑧𝑆𝑘𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
195194ad2antlr 727 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
19617, 190, 195mpbi2and 712 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st𝑧) = (1st𝑘))
197 eqtr3 2763 . . . . . 6 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → (2nd𝑧) = (2nd𝑘))
198197adantl 485 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd𝑧) = (2nd𝑘))
199 xpopth 7802 . . . . . . 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 599 . . . . . 6 ((𝑧𝑆𝑘𝑆) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
201200ad2antlr 727 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
202196, 198, 201mpbi2and 712 . . . 4 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧 = 𝑘)
203202ex 416 . . 3 ((𝜑 ∧ (𝑧𝑆𝑘𝑆)) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
204203ralrimivva 3112 . 2 (𝜑 → ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
205 fveqeq2 6726 . . 3 (𝑧 = 𝑘 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑘) = 𝑁))
206205rmo4 3643 . 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 847   = wceq 1543  wcel 2110  {cab 2714  wne 2940  wral 3061  ∃*wrmo 3064  {crab 3065  csb 3811  cdif 3863  cun 3864  cin 3865  c0 4237  ifcif 4439  {csn 4541   class class class wbr 5053  cmpt 5135   × cxp 5549  ccnv 5550  cima 5554  Fun wfun 6374   Fn wfn 6375  wf 6376  ontowfo 6378  1-1-ontowf1o 6379  cfv 6380  (class class class)co 7213  f cof 7467  1st c1st 7759  2nd c2nd 7760  m cmap 8508  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   < clt 10867  cle 10868  cmin 11062  cn 11830  cz 12176  cuz 12438  ...cfz 13095  ..^cfzo 13238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096  df-fzo 13239
This theorem is referenced by:  poimirlem18  35532  poimirlem21  35535
  Copyright terms: Public domain W3C validator