Theorem poimirlem18 35795

Description: Lemma for poimir 35810 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (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...𝑁)))
poimirlem22.2	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem18.3	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
poimirlem18.4	⊢ (𝜑 → (2nd ‘𝑇) = 0)

Assertion

Ref	Expression
poimirlem18	⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Distinct variable groups:   𝑓,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑝,𝑡   𝑓,𝐾,𝑗,𝑛,𝑝,𝑡   𝑓,𝑁,𝑝,𝑡   𝑇,𝑓,𝑝   𝜑,𝑧   𝑓,𝐹,𝑝,𝑡,𝑧   𝑧,𝐾   𝑧,𝑁   𝑡,𝑇,𝑧   𝑆,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem18

Dummy variable 𝑠 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		poimirlem22.s	. . 3 ⊢ 𝑆 = {𝑡 ∈ ((((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}))))}
3		poimirlem22.1	. . 3 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
4		poimirlem22.2	. . 3 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
5		poimirlem18.3	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
6		poimirlem18.4	. . 3 ⊢ (𝜑 → (2nd ‘𝑇) = 0)
7	1, 2, 3, 4, 5, 6	poimirlem17 35794	. 2 ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
8	6	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2nd ‘𝑇) = 0)
9		0nnn 12009	. . . . . . . . . . . . 13 ⊢ ¬ 0 ∈ ℕ
10		elfznn 13285	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 0 ∈ ℕ)
11	9, 10	mto 196	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
12		eleq1 2826	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑧) = 0 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1))))
13	11, 12	mtbiri 327	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑧) = 0 → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))
14	13	necon2ai 2973	. . . . . . . . . 10 ⊢ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd ‘𝑧) ≠ 0)
15	1	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
16		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧))
17	16	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧)))
18	17	ifbid 4482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)))
19	18	csbeq1d 3836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
20		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → (1st ‘(1st ‘𝑡)) = (1st ‘(1st ‘𝑧)))
21		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → (2nd ‘(1st ‘𝑡)) = (2nd ‘(1st ‘𝑧)))
22	21	imaeq1d 5968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → ((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st ‘𝑧)) “ (1...𝑗)))
23	22	xpeq1d 5618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}))
24	21	imaeq1d 5968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → ((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
25	24	xpeq1d 5618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
26	23, 25	uneq12d 4098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
27	20, 26	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
28	27	csbeq2dv 3839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
29	19, 28	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
30	29	mpteq2dv 5176	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
31	30	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
32	31, 2	elrab2 3627	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((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}))))))
33	32	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
34	33	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑧)) ∘f + ((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
35		elrabi 3618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑡 ∈ ((((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...𝑁)))
36	35, 2	eleq2s 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
37		xp1st 7863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
39		xp1st 7863	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
41		elmapi 8637	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
42	40, 41	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
43		elfzoelz 13387	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
44	43	ssriv 3925	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
45		fss 6617	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st ‘𝑧)):(1...𝑁)⟶ℤ)
46	42, 44, 45	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → (1st ‘(1st ‘𝑧)):(1...𝑁)⟶ℤ)
47	46	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1st ‘(1st ‘𝑧)):(1...𝑁)⟶ℤ)
48		xp2nd 7864	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
49	38, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
50		fvex 6787	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘(1st ‘𝑧)) ∈ V
51		f1oeq1 6704	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2nd ‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
52	50, 51	elab 3609	. . . . . . . . . . . . . . . 16 ⊢ ((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
53	49, 52	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → (2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
54	53	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
55		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))
56	15, 34, 47, 54, 55	poimirlem1 35778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))
57	1	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → 𝑁 ∈ ℕ)
58		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇))
59	58	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇)))
60	59	ifbid 4482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)))
61	60	csbeq1d 3836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
62		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (1st ‘(1st ‘𝑡)) = (1st ‘(1st ‘𝑇)))
63		2fveq3 6779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑇 → (2nd ‘(1st ‘𝑡)) = (2nd ‘(1st ‘𝑇)))
64	63	imaeq1d 5968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 𝑇 → ((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st ‘𝑇)) “ (1...𝑗)))
65	64	xpeq1d 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}))
66	63	imaeq1d 5968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 𝑇 → ((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
67	66	xpeq1d 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
68	65, 67	uneq12d 4098	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
69	62, 68	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
70	69	csbeq2dv 3839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
71	61, 70	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
72	71	mpteq2dv 5176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
73	72	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
74	73, 2	elrab2 3627	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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}))))))
75	74	simprbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
76	4, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
77	76	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑇)) ∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
78		elrabi 3618	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁)))
79	78, 2	eleq2s 2857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
80	4, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
81		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
83		xp1st 7863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
85		elmapi 8637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
87		fss 6617	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st ‘(1st ‘𝑇)):(1...𝑁)⟶ℤ)
88	86, 44, 87	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1st ‘(1st ‘𝑇)):(1...𝑁)⟶ℤ)
89	88	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → (1st ‘(1st ‘𝑇)):(1...𝑁)⟶ℤ)
90		xp2nd 7864	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
91	82, 90	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
92		fvex 6787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘(1st ‘𝑇)) ∈ V
93		f1oeq1 6704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (2nd ‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
94	92, 93	elab 3609	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
95	91, 94	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
96	95	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → (2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
97		simplr 766	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))
98		xp2nd 7864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁))
99	80, 98	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2nd ‘𝑇) ∈ (0...𝑁))
100	99	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘𝑇) ∈ (0...𝑁))
101		eldifsn 4720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}) ↔ ((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)))
102	101	biimpri 227	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}))
103	100, 102	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}))
104	57, 77, 89, 96, 97, 103	poimirlem2 35779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2nd ‘𝑇) ≠ (2nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))
105	104	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd ‘𝑇) ≠ (2nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)))
106	105	necon1bd 2961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧)))
107	106	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧)))
108	56, 107	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd ‘𝑇) = (2nd ‘𝑧))
109	108	neeq1d 3003	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd ‘𝑇) ≠ 0 ↔ (2nd ‘𝑧) ≠ 0))
110	109	exbiri 808	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2nd ‘𝑧) ≠ 0 → (2nd ‘𝑇) ≠ 0)))
111	14, 110	mpdi 45	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd ‘𝑇) ≠ 0))
112	111	necon2bd 2959	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑇) = 0 → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))))
113	8, 112	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))
114		xp2nd 7864	. . . . . . . . 9 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁))
115	36, 114	syl 17	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁))
116	1	nncnd 11989	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
117		npcan1 11400	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
119		nnuz 12621	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℤ≥‘1)
120	1, 119	eleqtrdi 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
121	118, 120	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘1))
122	1	nnzd 12425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
123		peano2zm 12363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
125		uzid 12597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
126		peano2uz 12641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
127	124, 125, 126	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
128	118, 127	eqeltrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1)))
129		fzsplit2 13281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
130	121, 128, 129	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
131	118	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
132		fzsn 13298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
133	122, 132	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
134	131, 133	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
135	134	uneq2d 4097	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
136	130, 135	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
137	136	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2nd ‘𝑧) ∈ (1...𝑁) ↔ (2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
138	137	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (2nd ‘𝑧) ∈ (1...𝑁) ↔ ¬ (2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
139		ioran 981	. . . . . . . . . . . . . 14 ⊢ (¬ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd ‘𝑧) = 𝑁) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁))
140		elun 4083	. . . . . . . . . . . . . . 15 ⊢ ((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd ‘𝑧) ∈ {𝑁}))
141		fvex 6787	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑧) ∈ V
142	141	elsn 4576	. . . . . . . . . . . . . . . 16 ⊢ ((2nd ‘𝑧) ∈ {𝑁} ↔ (2nd ‘𝑧) = 𝑁)
143	142	orbi2i 910	. . . . . . . . . . . . . . 15 ⊢ (((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd ‘𝑧) ∈ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd ‘𝑧) = 𝑁))
144	140, 143	bitri 274	. . . . . . . . . . . . . 14 ⊢ ((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd ‘𝑧) = 𝑁))
145	139, 144	xchnxbir 333	. . . . . . . . . . . . 13 ⊢ (¬ (2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁))
146	138, 145	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ (2nd ‘𝑧) ∈ (1...𝑁) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁)))
147	146	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝜑 → (((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁)) ↔ ((2nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁))))
148	1	nnnn0d 12293	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
149		nn0uz 12620	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 = (ℤ≥‘0)
150	148, 149	eleqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘0))
151		fzpred 13304	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
152	150, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
153	152	difeq1d 4056	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)))
154		difun2 4414	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...𝑁)) = ({0} ∖ (1...𝑁))
155		0p1e1 12095	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
156	155	oveq1i 7285	. . . . . . . . . . . . . . . . 17 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
157	156	uneq2i 4094	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
158	157	difeq1i 4053	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = (({0} ∪ (1...𝑁)) ∖ (1...𝑁))
159		incom 4135	. . . . . . . . . . . . . . . . 17 ⊢ ({0} ∩ (1...𝑁)) = ((1...𝑁) ∩ {0})
160		elfznn 13285	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ (1...𝑁) → 0 ∈ ℕ)
161	9, 160	mto 196	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 0 ∈ (1...𝑁)
162		disjsn 4647	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑁) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...𝑁))
163	161, 162	mpbir 230	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑁) ∩ {0}) = ∅
164	159, 163	eqtri 2766	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∩ (1...𝑁)) = ∅
165		disj3 4387	. . . . . . . . . . . . . . . 16 ⊢ (({0} ∩ (1...𝑁)) = ∅ ↔ {0} = ({0} ∖ (1...𝑁)))
166	164, 165	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ {0} = ({0} ∖ (1...𝑁))
167	154, 158, 166	3eqtr4i 2776	. . . . . . . . . . . . . 14 ⊢ (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = {0}
168	153, 167	eqtrdi 2794	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0})
169	168	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ (2nd ‘𝑧) ∈ {0}))
170		eldif 3897	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁)))
171	141	elsn 4576	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑧) ∈ {0} ↔ (2nd ‘𝑧) = 0)
172	169, 170, 171	3bitr3g 313	. . . . . . . . . . 11 ⊢ (𝜑 → (((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁)) ↔ (2nd ‘𝑧) = 0))
173	147, 172	bitr3d 280	. . . . . . . . . 10 ⊢ (𝜑 → (((2nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁)) ↔ (2nd ‘𝑧) = 0))
174	173	biimpd 228	. . . . . . . . 9 ⊢ (𝜑 → (((2nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁)) → (2nd ‘𝑧) = 0))
175	174	expdimp 453	. . . . . . . 8 ⊢ ((𝜑 ∧ (2nd ‘𝑧) ∈ (0...𝑁)) → ((¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0))
176	115, 175	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0))
177	113, 176	mpand 692	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → (2nd ‘𝑧) = 0))
178	1, 2, 3	poimirlem13 35790	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0)
179		fveqeq2 6783	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → ((2nd ‘𝑧) = 0 ↔ (2nd ‘𝑠) = 0))
180	179	rmo4 3665	. . . . . . . . . 10 ⊢ (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0 ↔ ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠))
181	178, 180	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠))
182	181	r19.21bi 3134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠))
183	4	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆)
184		fveqeq2 6783	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑇 → ((2nd ‘𝑠) = 0 ↔ (2nd ‘𝑇) = 0))
185	184	anbi2d 629	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) ↔ ((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑇) = 0)))
186		eqeq2 2750	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇))
187	185, 186	imbi12d 345	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑇) = 0) → 𝑧 = 𝑇)))
188	187	rspccv 3558	. . . . . . . 8 ⊢ (∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑇) = 0) → 𝑧 = 𝑇)))
189	182, 183, 188	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑇) = 0) → 𝑧 = 𝑇))
190	8, 189	mpan2d 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) = 0 → 𝑧 = 𝑇))
191	177, 190	syld 47	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇))
192	191	necon1ad 2960	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁))
193	192	ralrimiva 3103	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁))
194	1, 2, 3	poimirlem14 35791	. . 3 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁)
195		rmoim 3675	. . 3 ⊢ (∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁) → (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇))
196	193, 194, 195	sylc 65	. 2 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
197		reu5 3361	. 2 ⊢ (∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇))
198	7, 196, 197	sylanbrc 583	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  ∃*wrmo 3067  {crab 3068  ⦋csb 3832   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459  {csn 4561   class class class wbr 5074   ↦ cmpt 5157   × cxp 5587  ran crn 5590   “ cima 5592  ⟶wf 6429  –1-1-onto→wf1o 6432  ‘cfv 6433  (class class class)co 7275   ∘_f cof 7531  1^st c1st 7829  2^nd c2nd 7830   ↑_m cmap 8615  ℂcc 10869  0cc0 10871  1c1 10872   + caddc 10874   < clt 11009   − cmin 11205  ℕcn 11973  ℕ₀cn0 12233  ℤcz 12319  ℤ_≥cuz 12582  ...cfz 13239  ..^cfzo 13382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383

This theorem is referenced by:  poimirlem22  35799