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 33738
Description: Lemma for poimir 33757- 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 708 . . . . . . . 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 786 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧𝑆)
51nngt0d 11353 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
6 breq2 4855 . . . . . . . . . . 11 ((2nd𝑧) = 𝑁 → (0 < (2nd𝑧) ↔ 0 < 𝑁))
76biimparc 467 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
85, 7sylan 571 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑧) = 𝑁) → 0 < (2nd𝑧))
98ad2ant2r 744 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑧))
102, 3, 4, 9poimirlem5 33729 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑧)))
11 simplrr 787 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑘𝑆)
12 breq2 4855 . . . . . . . . . . 11 ((2nd𝑘) = 𝑁 → (0 < (2nd𝑘) ↔ 0 < 𝑁))
1312biimparc 467 . . . . . . . . . 10 ((0 < 𝑁 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
145, 13sylan 571 . . . . . . . . 9 ((𝜑 ∧ (2nd𝑘) = 𝑁) → 0 < (2nd𝑘))
1514ad2ant2rl 746 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 0 < (2nd𝑘))
162, 3, 11, 15poimirlem5 33729 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (𝐹‘0) = (1st ‘(1st𝑘)))
1710, 16eqtr3d 2849 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st ‘(1st𝑧)) = (1st ‘(1st𝑘)))
18 elrabi 3561 . . . . . . . . . . . . 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 2910 . . . . . . . . . . . 12 (𝑧𝑆𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
20 xp1st 7433 . . . . . . . . . . . 12 (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
21 xp2nd 7434 . . . . . . . . . . . 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 6424 . . . . . . . . . . . 12 (2nd ‘(1st𝑧)) ∈ V
24 f1oeq1 6346 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
2523, 24elab 3552 . . . . . . . . . . 11 ((2nd ‘(1st𝑧)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
2622, 25sylib 209 . . . . . . . . . 10 (𝑧𝑆 → (2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
27 f1ofn 6357 . . . . . . . . . 10 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2826, 27syl 17 . . . . . . . . 9 (𝑧𝑆 → (2nd ‘(1st𝑧)) Fn (1...𝑁))
2928adantr 468 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
3029ad2antlr 709 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) Fn (1...𝑁))
31 elrabi 3561 . . . . . . . . . . . . 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 2910 . . . . . . . . . . . 12 (𝑘𝑆𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33 xp1st 7433 . . . . . . . . . . . 12 (𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp2nd 7434 . . . . . . . . . . . 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 6424 . . . . . . . . . . . 12 (2nd ‘(1st𝑘)) ∈ V
37 f1oeq1 6346 . . . . . . . . . . . 12 (𝑓 = (2nd ‘(1st𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
3836, 37elab 3552 . . . . . . . . . . 11 ((2nd ‘(1st𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
3935, 38sylib 209 . . . . . . . . . 10 (𝑘𝑆 → (2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
40 f1ofn 6357 . . . . . . . . . 10 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4139, 40syl 17 . . . . . . . . 9 (𝑘𝑆 → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4241adantl 469 . . . . . . . 8 ((𝑧𝑆𝑘𝑆) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
4342ad2antlr 709 . . . . . . 7 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑘)) Fn (1...𝑁))
44 simpllr 784 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧𝑆𝑘𝑆))
45 oveq2 6885 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
4645imaeq2d 5683 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑧)) “ (1...𝑁)))
47 f1ofo 6363 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁))
48 foima 6339 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
4926, 47, 483syl 18 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((2nd ‘(1st𝑧)) “ (1...𝑁)) = (1...𝑁))
5046, 49sylan9eqr 2869 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5150adantlr 697 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = (1...𝑁))
5245imaeq2d 5683 . . . . . . . . . . . . . . 15 (𝑛 = 𝑁 → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑁)))
53 f1ofo 6363 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁))
54 foima 6339 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5539, 53, 543syl 18 . . . . . . . . . . . . . . 15 (𝑘𝑆 → ((2nd ‘(1st𝑘)) “ (1...𝑁)) = (1...𝑁))
5652, 55sylan9eqr 2869 . . . . . . . . . . . . . 14 ((𝑘𝑆𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5756adantll 696 . . . . . . . . . . . . 13 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑘)) “ (1...𝑛)) = (1...𝑁))
5851, 57eqtr4d 2850 . . . . . . . . . . . 12 (((𝑧𝑆𝑘𝑆) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
5944, 58sylan 571 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
60 simpll 774 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝜑)
61 elnnuz 11945 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
621, 61sylib 209 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
63 fzm1 12646 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁)))
6564anbi1d 617 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁)))
6665biimpa 464 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁))
67 df-ne 2986 . . . . . . . . . . . . . . . . . 18 (𝑛𝑁 ↔ ¬ 𝑛 = 𝑁)
6867anbi2i 611 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁))
69 pm5.61 1014 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7068, 69bitri 266 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
7166, 70sylib 209 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁))
72 fz1ssfz0 12662 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
7372sseli 3801 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ (0...(𝑁 − 1)))
7473adantr 468 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁) → 𝑛 ∈ (0...(𝑁 − 1)))
7571, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
7660, 75sylan 571 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → 𝑛 ∈ (0...(𝑁 − 1)))
77 eleq1 2880 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1))))
7877anbi2d 616 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1)))))
79 oveq2 6885 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
8079imaeq2d 5683 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...𝑛)))
8179imaeq2d 5683 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
8280, 81eqeq12d 2828 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛))))
8378, 82imbi12d 335 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚))) ↔ ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))))
841ad3antrrr 712 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ)
85 poimirlem22.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
8685ad3antrrr 712 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
87 simpl 470 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑧𝑆)
8887ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧𝑆)
89 simplrl 786 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑧) = 𝑁)
90 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝑧𝑆𝑘𝑆) → 𝑘𝑆)
9190ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘𝑆)
92 simplrr 787 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd𝑘) = 𝑁)
93 simpr 473 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1)))
9484, 3, 86, 88, 89, 91, 92, 93poimirlem12 33736 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9584, 3, 86, 91, 92, 88, 89, 93poimirlem12 33736 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) ⊆ ((2nd ‘(1st𝑧)) “ (1...𝑚)))
9694, 95eqssd 3822 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)))
9783, 96chvarv 2439 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9876, 97syldan 581 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
9998anassrs 455 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛𝑁) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
10059, 99pm2.61dane 3072 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
101 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
102 elfzelz 12568 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1031nnzd 11750 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
104 elfzm1b 12644 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
105102, 103, 104syl2anr 586 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
106101, 105mpbid 223 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
10760, 106sylan 571 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))
108 ovex 6909 . . . . . . . . . . . 12 (𝑛 − 1) ∈ V
109 eleq1 2880 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
110109anbi2d 616 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
111 oveq2 6885 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1)))
112111imaeq2d 5683 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))
113111imaeq2d 5683 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → ((2nd ‘(1st𝑘)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
114112, 113eqeq12d 2828 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → (((2nd ‘(1st𝑧)) “ (1...𝑚)) = ((2nd ‘(1st𝑘)) “ (1...𝑚)) ↔ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
115110, 114imbi12d 335 . . . . . . . . . . . 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 3459 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
117107, 116syldan 581 . . . . . . . . . 10 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
118100, 117difeq12d 3935 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
119 fnsnfv 6482 . . . . . . . . . . . 12 (((2nd ‘(1st𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
12028, 119sylan 571 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = ((2nd ‘(1st𝑧)) “ {𝑛}))
121 elfznn 12596 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
122 uncom 3963 . . . . . . . . . . . . . . . . 17 ((1...(𝑛 − 1)) ∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1)))
123122difeq1i 3930 . . . . . . . . . . . . . . . 16 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1)))
124 difun2 4251 . . . . . . . . . . . . . . . 16 (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
125123, 124eqtri 2835 . . . . . . . . . . . . . . 15 (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1)))
126 nncn 11316 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
127 npcan1 10743 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
128126, 127syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛)
129 elnnuz 11945 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
130129biimpi 207 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
131128, 130eqeltrd 2892 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
132 nnm1nn0 11603 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
133132nn0zd 11749 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℤ)
134 uzid 11922 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
135 peano2uz 11962 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
136133, 134, 1353syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
137128, 136eqeltrrd 2893 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
138 fzsplit2 12592 . . . . . . . . . . . . . . . . . 18 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
139131, 137, 138syl2anc 575 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
140128oveq1d 6892 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
141 nnz 11668 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
142 fzsn 12609 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛})
144140, 143eqtrd 2847 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
145144uneq2d 3973 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
146139, 145eqtrd 2847 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
147146difeq1d 3933 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = (((1...(𝑛 − 1)) ∪ {𝑛}) ∖ (1...(𝑛 − 1))))
148 nnre 11315 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
149 ltm1 11151 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
150 peano2rem 10636 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
151 ltnle 10405 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
152150, 151mpancom 671 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
153149, 152mpbid 223 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
154 elfzle2 12571 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1))
155153, 154nsyl 137 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
156148, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ¬ 𝑛 ∈ (1...(𝑛 − 1)))
157 incom 4011 . . . . . . . . . . . . . . . . . 18 ((1...(𝑛 − 1)) ∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1)))
158157eqeq1i 2818 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ({𝑛} ∩ (1...(𝑛 − 1))) = ∅)
159 disjsn 4445 . . . . . . . . . . . . . . . . 17 (((1...(𝑛 − 1)) ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ (1...(𝑛 − 1)))
160 disj3 4225 . . . . . . . . . . . . . . . . 17 (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
161158, 159, 1603bitr3i 292 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
162156, 161sylib 209 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1))))
163125, 147, 1623eqtr4a 2873 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
164121, 163syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛})
165164imaeq2d 5683 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
166165adantl 469 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd ‘(1st𝑧)) “ {𝑛}))
167 dff1o3 6362 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑧))))
168167simprbi 486 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑧)))
169 imadif 6187 . . . . . . . . . . . . 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 468 . . . . . . . . . . 11 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
172120, 166, 1713eqtr2d 2853 . . . . . . . . . 10 ((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
1734, 172sylan 571 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))))
174 eleq1 2880 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (𝑧𝑆𝑘𝑆))
175174anbi1d 617 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ((𝑧𝑆𝑛 ∈ (1...𝑁)) ↔ (𝑘𝑆𝑛 ∈ (1...𝑁))))
176 2fveq3 6416 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
177176fveq1d 6413 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
178177sneqd 4389 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
179176imaeq1d 5682 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...𝑛)) = ((2nd ‘(1st𝑘)) “ (1...𝑛)))
180176imaeq1d 5682 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))) = ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))
181179, 180difeq12d 3935 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
182178, 181eqeq12d 2828 . . . . . . . . . . . 12 (𝑧 = 𝑘 → ({((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1))))))
183175, 182imbi12d 335 . . . . . . . . . . 11 (𝑧 = 𝑘 → (((𝑧𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = (((2nd ‘(1st𝑧)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))))
184183, 172chvarv 2439 . . . . . . . . . 10 ((𝑘𝑆𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
18511, 184sylan 571 . . . . . . . . 9 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑘))‘𝑛)} = (((2nd ‘(1st𝑘)) “ (1...𝑛)) ∖ ((2nd ‘(1st𝑘)) “ (1...(𝑛 − 1)))))
186118, 173, 1853eqtr4d 2857 . . . . . . . 8 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)})
187 fvex 6424 . . . . . . . . 9 ((2nd ‘(1st𝑧))‘𝑛) ∈ V
188187sneqr 4566 . . . . . . . 8 ({((2nd ‘(1st𝑧))‘𝑛)} = {((2nd ‘(1st𝑘))‘𝑛)} → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
189186, 188syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd ‘(1st𝑧))‘𝑛) = ((2nd ‘(1st𝑘))‘𝑛))
19030, 43, 189eqfnfvd 6539 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘)))
19119, 20syl 17 . . . . . . . 8 (𝑧𝑆 → (1st𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
19232, 33syl 17 . . . . . . . 8 (𝑘𝑆 → (1st𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
193 xpopth 7442 . . . . . . . 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𝑘)))
194191, 192, 193syl2an 585 . . . . . . 7 ((𝑧𝑆𝑘𝑆) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
195194ad2antlr 709 . . . . . 6 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st ‘(1st𝑧)) = (1st ‘(1st𝑘)) ∧ (2nd ‘(1st𝑧)) = (2nd ‘(1st𝑘))) ↔ (1st𝑧) = (1st𝑘)))
19617, 190, 195mpbi2and 694 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (1st𝑧) = (1st𝑘))
197 eqtr3 2834 . . . . . 6 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → (2nd𝑧) = (2nd𝑘))
198197adantl 469 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (2nd𝑧) = (2nd𝑘))
199 xpopth 7442 . . . . . . 7 ((𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
20019, 32, 199syl2an 585 . . . . . 6 ((𝑧𝑆𝑘𝑆) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
201200ad2antlr 709 . . . . 5 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → (((1st𝑧) = (1st𝑘) ∧ (2nd𝑧) = (2nd𝑘)) ↔ 𝑧 = 𝑘))
202196, 198, 201mpbi2and 694 . . . 4 (((𝜑 ∧ (𝑧𝑆𝑘𝑆)) ∧ ((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁)) → 𝑧 = 𝑘)
203202ex 399 . . 3 ((𝜑 ∧ (𝑧𝑆𝑘𝑆)) → (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
204203ralrimivva 3166 . 2 (𝜑 → ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
205 fveqeq2 6420 . . 3 (𝑧 = 𝑘 → ((2nd𝑧) = 𝑁 ↔ (2nd𝑘) = 𝑁))
206205rmo4 3604 . 2 (∃*𝑧𝑆 (2nd𝑧) = 𝑁 ↔ ∀𝑧𝑆𝑘𝑆 (((2nd𝑧) = 𝑁 ∧ (2nd𝑘) = 𝑁) → 𝑧 = 𝑘))
207204, 206sylibr 225 1 (𝜑 → ∃*𝑧𝑆 (2nd𝑧) = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  {cab 2799  wne 2985  wral 3103  ∃*wrmo 3106  {crab 3107  csb 3735  cdif 3773  cun 3774  cin 3775  c0 4123  ifcif 4286  {csn 4377   class class class wbr 4851  cmpt 4930   × cxp 5316  ccnv 5317  cima 5321  Fun wfun 6098   Fn wfn 6099  wf 6100  ontowfo 6102  1-1-ontowf1o 6103  cfv 6104  (class class class)co 6877  𝑓 cof 7128  1st c1st 7399  2nd c2nd 7400  𝑚 cmap 8095  cc 10222  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   < clt 10362  cle 10363  cmin 10554  cn 11308  cz 11646  cuz 11907  ...cfz 12552  ..^cfzo 12692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-map 8097  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-nn 11309  df-n0 11563  df-z 11647  df-uz 11908  df-fz 12553  df-fzo 12693
This theorem is referenced by:  poimirlem18  33742  poimirlem21  33745
  Copyright terms: Public domain W3C validator