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 33082
Description: Lemma for poimir 33101- 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 761 . . . . . . . 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 799 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧𝑆)
51nngt0d 11015 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
6 breq2 4622 . . . . . . . . . . 11 ((2nd𝑧) = 𝑁 → (0 < (2nd𝑧) ↔ 0 < 𝑁))
76biimparc 504 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
85, 7sylan 488 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
98ad2ant2r 782 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑧))
102, 3, 4, 9poimirlem5 33073 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑧)))
11 simplrr 800 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑘𝑆)
12 breq2 4622 . . . . . . . . . . 11 ((2nd𝑘) = 𝑁 → (0 < (2nd𝑘) ↔ 0 < 𝑁))
1312biimparc 504 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
145, 13sylan 488 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
1514ad2ant2rl 784 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑘))
162, 3, 11, 15poimirlem5 33073 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑘)))
1710, 16eqtr3d 2657 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑘)))
18 elrabi 3346 . . . . . . . . . . . . 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 2716 . . . . . . . . . . . 12 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
20 xp1st 7150 . . . . . . . . . . . 12 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
21 xp2nd 7151 . . . . . . . . . . . 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 6163 . . . . . . . . . . . 12 (2nd ‘(1st𝑧)) ∈ V
24 f1oeq1 6089 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
2523, 24elab 3337 . . . . . . . . . . 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 6100 . . . . . . . . . 10 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2826, 27syl 17 . . . . . . . . 9 (𝑧𝑆 → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2928adantr 481 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
3029ad2antlr 762 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
31 elrabi 3346 . . . . . . . . . . . . 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 2716 . . . . . . . . . . . 12 (𝑘𝑆𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33 xp1st 7150 . . . . . . . . . . . 12 (𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp2nd 7151 . . . . . . . . . . . 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 6163 . . . . . . . . . . . 12 (2nd ‘(1st𝑘)) ∈ V
37 f1oeq1 6089 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
3836, 37elab 3337 . . . . . . . . . . 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 6100 . . . . . . . . . 10 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4139, 40syl 17 . . . . . . . . 9 (𝑘𝑆 → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4241adantl 482 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4342ad2antlr 762 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
44 simpllr 798 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧𝑆𝑘𝑆))
45 oveq2 6618 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
4645imaeq2d 5430 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
47 f1ofo 6106 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
48 foima 6082 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
4926, 47, 483syl 18 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
5046, 49sylan9eqr 2677 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5150adantlr 750 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5245imaeq2d 5430 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑁)))
53 f1ofo 6106 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁))
54 foima 6082 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5539, 53, 543syl 18 . . . . . . . . . . . . . . 15 (𝑘𝑆 → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5652, 55sylan9eqr 2677 . . . . . . . . . . . . . 14 ((𝑘𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5756adantll 749 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5851, 57eqtr4d 2658 . . . . . . . . . . . 12 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
5944, 58sylan 488 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
60 simpll 789 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝜑)
61 elnnuz 11675 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
621, 61sylib 208 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
63 fzm1 12368 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6564anbi1d 740 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁)))
6665biimpa 501 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁))
67 df-ne 2791 . . . . . . . . . . . . . . . . . 18 (𝑛𝑁 ↔ ¬ 𝑛 = 𝑁)
6867anbi2i 729 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁))
69 pm5.61 748 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7068, 69bitri 264 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7166, 70sylib 208 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
72 1eluzge0 11683 . . . . . . . . . . . . . . . . . 18 1 ∈ (ℤ‘0)
73 fzss1 12329 . . . . . . . . . . . . . . . . . 18 (1 ∈ (ℤ‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
7574sseli 3583 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ (0...(𝑁 − 1)))
7675adantr 481 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁) → 𝑛 ∈ (0...(𝑁 − 1)))
7771, 76syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
7860, 77sylan 488 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
79 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1))))
8079anbi2d 739 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1)))))
81 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
8281imaeq2d 5430 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...𝑛)))
8381imaeq2d 5430 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
8482, 83eqeq12d 2636 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛))))
8580, 84imbi12d 334 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚))) ↔ ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))))
861ad3antrrr 765 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
87 poimirlem22.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
8887ad3antrrr 765 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
89 simpl 473 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑧𝑆)
9089ad3antlr 766 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧𝑆)
91 simplrl 799 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑧) = 𝑁)
92 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑘𝑆)
9392ad3antlr 766 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘𝑆)
94 simplrr 800 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑘) = 𝑁)
95 simpr 477 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1)))
9686, 3, 88, 90, 91, 93, 94, 95poimirlem12 33080 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9786, 3, 88, 93, 94, 90, 91, 95poimirlem12 33080 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑧)) “ (1...𝑚)))
9896, 97eqssd 3604 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9985, 98chvarv 2262 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
10078, 99syldan 487 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
101100anassrs 679 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
10259, 101pm2.61dane 2877 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
103 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
104 elfzelz 12291 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1051nnzd 11432 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
106 elfzm1b 12366 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
107104, 105, 106syl2anr 495 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
108103, 107mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
10960, 108sylan 488 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
110 ovex 6638 . . . . . . . . . . . 12 (𝑛 − 1) ∈ V
111 eleq1 2686 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
112111anbi2d 739 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
113 oveq2 6618 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1)))
114113imaeq2d 5430 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))
115113imaeq2d 5430 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
116114, 115eqeq12d 2636 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
117112, 116imbi12d 334 . . . . . . . . . . . 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))))))
118110, 117, 98vtocl 3248 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
119109, 118syldan 487 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
120102, 119difeq12d 3712 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
121 fnsnfv 6220 . . . . . . . . . . . 12 (((2nd ‘(1st𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
12228, 121sylan 488 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
123 elfznn 12319 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
124 uncom 3740 . . . . . . . . . . . . . . . . 17 ((1...(𝑛 − 1)) ∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1)))
125124difeq1i 3707 . . . . . . . . . . . . . . . 16 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1)))
126 difun2 4025 . . . . . . . . . . . . . . . 16 (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
127125, 126eqtri 2643 . . . . . . . . . . . . . . 15 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
128 nncn 10979 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
129 npcan1 10406 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
130128, 129syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛)
131 elnnuz 11675 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
132131biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
133130, 132eqeltrd 2698 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
134 nnm1nn0 11285 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
135134nn0zd 11431 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℤ)
136 uzid 11653 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
137 peano2uz 11692 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
138135, 136, 1373syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
139130, 138eqeltrrd 2699 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
140 fzsplit2 12315 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
141133, 139, 140syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
142130oveq1d 6625 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
143 nnz 11350 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
144 fzsn 12332 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
145143, 144syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛})
146142, 145eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
147146uneq2d 3750 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
148141, 147eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
149148difeq1d 3710 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))))
150 nnre 10978 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
151 ltm1 10814 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
152 peano2rem 10299 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
153 ltnle 10068 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
154152, 153mpancom 702 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
155151, 154mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
156 elfzle2 12294 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1))
157155, 156nsyl 135 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
158150, 157syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
159 incom 3788 . . . . . . . . . . . . . . . . . 18 ((1...(𝑛 − 1)) ∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1)))
160159eqeq1i 2626 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ({𝑛} ∩ (1...(𝑛 − 1))) = ∅)
161 disjsn 4221 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ (1...(𝑛 − 1)))
162 disj3 3998 . . . . . . . . . . . . . . . . 17 (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
163160, 161, 1623bitr3i 290 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
164158, 163sylib 208 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
165127, 149, 1643eqtr4a 2681 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
166123, 165syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
167166imaeq2d 5430 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
168167adantl 482 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
169 dff1o3 6105 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑧))))
170169simprbi 480 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑧)))
171 imadif 5936 . . . . . . . . . . . . 13 (Fun (2nd ‘(1st𝑧)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
17226, 170, 1713syl 18 . . . . . . . . . . . 12 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
173172adantr 481 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
174122, 168, 1733eqtr2d 2661 . . . . . . . . . 10 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
1754, 174sylan 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
176 eleq1 2686 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (𝑧𝑆𝑘𝑆))
177176anbi1d 740 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ((𝑧𝑆𝑛 ∈ (1...𝑁)) ↔ (𝑘𝑆𝑛 ∈ (1...𝑁))))
178 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑘 → (1st𝑧) = (1st𝑘))
179178fveq2d 6157 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
180179fveq1d 6155 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
181180sneqd 4165 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
182179imaeq1d 5429 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
183179imaeq1d 5429 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
184182, 183difeq12d 3712 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
185181, 184eqeq12d 2636 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ({((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))))
186177, 185imbi12d 334 . . . . . . . . . . 11 (𝑧 = 𝑘 → (((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))))
187186, 174chvarv 2262 . . . . . . . . . 10 ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
18811, 187sylan 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
189120, 175, 1883eqtr4d 2665 . . . . . . . 8 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
190 fvex 6163 . . . . . . . . 9 ((2nd ‘(1st𝑧))‘𝑛) ∈ V
191190sneqr 4344 . . . . . . . 8 ({((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)} → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
192189, 191syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
19330, 43, 192eqfnfvd 6275 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
19419, 20syl 17 . . . . . . . 8 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
19532, 33syl 17 . . . . . . . 8 (𝑘𝑆 → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
196 xpopth 7159 . . . . . . . 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𝑘)))
197194, 195, 196syl2an 494 . . . . . . 7 ((𝑧𝑆𝑘𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
198197ad2antlr 762 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
19917, 193, 198mpbi2and 955 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st𝑧) = (1st𝑘))
200 eqtr3 2642 . . . . . 6 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → (2nd𝑧) = (2nd𝑘))
201200adantl 482 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd𝑧) = (2nd𝑘))
202 xpopth 7159 . . . . . . 7 ((𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
20319, 32, 202syl2an 494 . . . . . 6 ((𝑧𝑆𝑘𝑆) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
204203ad2antlr 762 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
205199, 201, 204mpbi2and 955 . . . 4 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧 = 𝑘)
206205ex 450 . . 3 ((𝜑 ∧ (𝑧𝑆𝑘𝑆)) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
207206ralrimivva 2966 . 2 (𝜑 → ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
208 fveq2 6153 . . . 4 (𝑧 = 𝑘 → (2nd𝑧) = (2nd𝑘))
209208eqeq1d 2623 . . 3 (𝑧 = 𝑘 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑘) = 𝑁))
210209rmo4 3385 . 2 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
211207, 210sylibr 224 1 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  {cab 2607  wne 2790  wral 2907  ∃*wrmo 2910  {crab 2911  csb 3518  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  ifcif 4063  {csn 4153   class class class wbr 4618  cmpt 4678   × cxp 5077  ccnv 5078  cima 5082  Fun wfun 5846   Fn wfn 5847  wf 5848  ontowfo 5850  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  𝑓 cof 6855  1st c1st 7118  2nd c2nd 7119  𝑚 cmap 7809  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   < clt 10025  cle 10026  cmin 10217  cn 10971  cz 11328  cuz 11638  ...cfz 12275  ..^cfzo 12413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-fzo 12414
This theorem is referenced by:  poimirlem18  33086  poimirlem21  33089
  Copyright terms: Public domain W3C validator