poimirlem18 - Mathbox for Brendan Leahy

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

Theorem poimirlem18 36506

Description: Lemma for poimir 36521 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(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1	⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
poimirlem22.2	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem18.3	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
poimirlem18.4	⊢ (𝜑 → (2^nd ‘𝑇) = 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(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 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 ⊢ (𝜑 → (2^nd ‘𝑇) = 0)
7	1, 2, 3, 4, 5, 6	poimirlem17 36505	. 2 ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
8	6	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑇) = 0)
9		0nnn 12248	. . . . . . . . . . . . 13 ⊢ ¬ 0 ∈ ℕ
10		elfznn 13530	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 0 ∈ ℕ)
11	9, 10	mto 196	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
12		eleq1 2822	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑧) = 0 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1))))
13	11, 12	mtbiri 327	. . . . . . . . . . 11 ⊢ ((2^nd ‘𝑧) = 0 → ¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
14	13	necon2ai 2971	. . . . . . . . . 10 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ≠ 0)
15	1	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
16		fveq2 6892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
17	16	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
18	17	ifbid 4552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
19	18	csbeq1d 3898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
20		2fveq3 6897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
21		2fveq3 6897	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
22	21	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
23	22	xpeq1d 5706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
24	21	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
25	24	xpeq1d 5706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
26	23, 25	uneq12d 4165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
27	20, 26	oveq12d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
28	27	csbeq2dv 3901	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
29	19, 28	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
30	29	mpteq2dv 5251	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
31	30	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
32	31, 2	elrab2 3687	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
33	32	simprbi 498	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
34	33	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
35		elrabi 3678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
36	35, 2	eleq2s 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
37		xp1st 8007	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
39		xp1st 8007	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
41		elmapi 8843	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
42	40, 41	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
43		elfzoelz 13632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
44	43	ssriv 3987	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
45		fss 6735	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
46	42, 44, 45	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
47	46	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
48		xp2nd 8008	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
49	38, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
50		fvex 6905	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
51		f1oeq1 6822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
52	50, 51	elab 3669	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
53	49, 52	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
54	53	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
55		simpr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
56	15, 34, 47, 54, 55	poimirlem1 36489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑧))‘𝑛))
57	1	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → 𝑁 ∈ ℕ)
58		fveq2 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
59	58	breq2d 5161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
60	59	ifbid 4552	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
61	60	csbeq1d 3898	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
62		2fveq3 6897	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
63		2fveq3 6897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
64	63	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
65	64	xpeq1d 5706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
66	63	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
67	66	xpeq1d 5706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
68	65, 67	uneq12d 4165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
69	62, 68	oveq12d 7427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
70	69	csbeq2dv 3901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
71	61, 70	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
72	71	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
73	72	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
74	73, 2	elrab2 3687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
75	74	simprbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
76	4, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
77	76	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
78		elrabi 3678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
79	78, 2	eleq2s 2852	. . . . . . . . . . . . . . . . . . . . . . 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 8007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
83		xp1st 8007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
85		elmapi 8843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
87		fss 6735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
88	86, 44, 87	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
89	88	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
90		xp2nd 8008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
91	82, 90	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
92		fvex 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
93		f1oeq1 6822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
94	92, 93	elab 3669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
95	91, 94	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
96	95	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
97		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
98		xp2nd 8008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑇) ∈ (0...𝑁))
99	80, 98	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
100	99	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (0...𝑁))
101		eldifsn 4791	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑧)}) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)))
102	101	biimpri 227	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑇) ∈ (0...𝑁) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → (2^nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑧)}))
103	100, 102	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → (2^nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑧)}))
104	57, 77, 89, 96, 97, 103	poimirlem2 36490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≠ (2^nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑧))‘𝑛))
105	104	ex 414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) ≠ (2^nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑧))‘𝑛)))
106	105	necon1bd 2959	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑧))‘𝑛) → (2^nd ‘𝑇) = (2^nd ‘𝑧)))
107	106	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑧))‘𝑛) → (2^nd ‘𝑇) = (2^nd ‘𝑧)))
108	56, 107	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) = (2^nd ‘𝑧))
109	108	neeq1d 3001	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) ≠ 0 ↔ (2^nd ‘𝑧) ≠ 0))
110	109	exbiri 810	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑧) ≠ 0 → (2^nd ‘𝑇) ≠ 0)))
111	14, 110	mpdi 45	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≠ 0))
112	111	necon2bd 2957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑇) = 0 → ¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
113	8, 112	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
114		xp2nd 8008	. . . . . . . . 9 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑧) ∈ (0...𝑁))
115	36, 114	syl 17	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘𝑧) ∈ (0...𝑁))
116	1	nncnd 12228	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
117		npcan1 11639	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
119		nnuz 12865	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℤ_≥‘1)
120	1, 119	eleqtrdi 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
121	118, 120	eqeltrd 2834	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
122	1	nnzd 12585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
123		peano2zm 12605	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
125		uzid 12837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
126		peano2uz 12885	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
127	124, 125, 126	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
128	118, 127	eqeltrrd 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
129		fzsplit2 13526	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
130	121, 128, 129	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
131	118	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
132		fzsn 13543	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
133	122, 132	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
134	131, 133	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
135	134	uneq2d 4164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
136	130, 135	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
137	136	eleq2d 2820	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘𝑧) ∈ (1...𝑁) ↔ (2^nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
138	137	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ (2^nd ‘𝑧) ∈ (1...𝑁) ↔ ¬ (2^nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁})))
139		ioran 983	. . . . . . . . . . . . . 14 ⊢ (¬ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2^nd ‘𝑧) = 𝑁) ↔ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁))
140		elun 4149	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2^nd ‘𝑧) ∈ {𝑁}))
141		fvex 6905	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘𝑧) ∈ V
142	141	elsn 4644	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑧) ∈ {𝑁} ↔ (2^nd ‘𝑧) = 𝑁)
143	142	orbi2i 912	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2^nd ‘𝑧) ∈ {𝑁}) ↔ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2^nd ‘𝑧) = 𝑁))
144	140, 143	bitri 275	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2^nd ‘𝑧) = 𝑁))
145	139, 144	xchnxbir 333	. . . . . . . . . . . . 13 ⊢ (¬ (2^nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁))
146	138, 145	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ (2^nd ‘𝑧) ∈ (1...𝑁) ↔ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁)))
147	146	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝜑 → (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑧) ∈ (1...𝑁)) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁))))
148	1	nnnn0d 12532	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
149		nn0uz 12864	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
150	148, 149	eleqtrdi 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
151		fzpred 13549	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
152	150, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
153	152	difeq1d 4122	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)))
154		difun2 4481	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...𝑁)) = ({0} ∖ (1...𝑁))
155		0p1e1 12334	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
156	155	oveq1i 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
157	156	uneq2i 4161	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
158	157	difeq1i 4119	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = (({0} ∪ (1...𝑁)) ∖ (1...𝑁))
159		incom 4202	. . . . . . . . . . . . . . . . 17 ⊢ ({0} ∩ (1...𝑁)) = ((1...𝑁) ∩ {0})
160		elfznn 13530	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ (1...𝑁) → 0 ∈ ℕ)
161	9, 160	mto 196	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 0 ∈ (1...𝑁)
162		disjsn 4716	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑁) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...𝑁))
163	161, 162	mpbir 230	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑁) ∩ {0}) = ∅
164	159, 163	eqtri 2761	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∩ (1...𝑁)) = ∅
165		disj3 4454	. . . . . . . . . . . . . . . 16 ⊢ (({0} ∩ (1...𝑁)) = ∅ ↔ {0} = ({0} ∖ (1...𝑁)))
166	164, 165	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ {0} = ({0} ∖ (1...𝑁))
167	154, 158, 166	3eqtr4i 2771	. . . . . . . . . . . . . 14 ⊢ (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁)) = {0}
168	153, 167	eqtrdi 2789	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0})
169	168	eleq2d 2820	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ (2^nd ‘𝑧) ∈ {0}))
170		eldif 3959	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑧) ∈ (1...𝑁)))
171	141	elsn 4644	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑧) ∈ {0} ↔ (2^nd ‘𝑧) = 0)
172	169, 170, 171	3bitr3g 313	. . . . . . . . . . 11 ⊢ (𝜑 → (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑧) ∈ (1...𝑁)) ↔ (2^nd ‘𝑧) = 0))
173	147, 172	bitr3d 281	. . . . . . . . . 10 ⊢ (𝜑 → (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁)) ↔ (2^nd ‘𝑧) = 0))
174	173	biimpd 228	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁)) → (2^nd ‘𝑧) = 0))
175	174	expdimp 454	. . . . . . . 8 ⊢ ((𝜑 ∧ (2^nd ‘𝑧) ∈ (0...𝑁)) → ((¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁) → (2^nd ‘𝑧) = 0))
176	115, 175	sylan2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2^nd ‘𝑧) = 𝑁) → (2^nd ‘𝑧) = 0))
177	113, 176	mpand 694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2^nd ‘𝑧) = 𝑁 → (2^nd ‘𝑧) = 0))
178	1, 2, 3	poimirlem13 36501	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2^nd ‘𝑧) = 0)
179		fveqeq2 6901	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → ((2^nd ‘𝑧) = 0 ↔ (2^nd ‘𝑠) = 0))
180	179	rmo4 3727	. . . . . . . . . 10 ⊢ (∃*𝑧 ∈ 𝑆 (2^nd ‘𝑧) = 0 ↔ ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) → 𝑧 = 𝑠))
181	178, 180	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) → 𝑧 = 𝑠))
182	181	r19.21bi 3249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) → 𝑧 = 𝑠))
183	4	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆)
184		fveqeq2 6901	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑇 → ((2^nd ‘𝑠) = 0 ↔ (2^nd ‘𝑇) = 0))
185	184	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) ↔ ((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑇) = 0)))
186		eqeq2 2745	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇))
187	185, 186	imbi12d 345	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑇) = 0) → 𝑧 = 𝑇)))
188	187	rspccv 3610	. . . . . . . 8 ⊢ (∀𝑠 ∈ 𝑆 (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑠) = 0) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑇) = 0) → 𝑧 = 𝑇)))
189	182, 183, 188	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2^nd ‘𝑧) = 0 ∧ (2^nd ‘𝑇) = 0) → 𝑧 = 𝑇))
190	8, 189	mpan2d 693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) = 0 → 𝑧 = 𝑇))
191	177, 190	syld 47	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2^nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇))
192	191	necon1ad 2958	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^nd ‘𝑧) = 𝑁))
193	192	ralrimiva 3147	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2^nd ‘𝑧) = 𝑁))
194	1, 2, 3	poimirlem14 36502	. . 3 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2^nd ‘𝑧) = 𝑁)
195		rmoim 3737	. . 3 ⊢ (∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2^nd ‘𝑧) = 𝑁) → (∃𝑧 ∈ 𝑆 (2^nd ‘𝑧) = 𝑁 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇))
196	193, 194, 195	sylc 65	. 2 ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
197		reu5 3379	. 2 ⊢ (∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇))
198	7, 196, 197	sylanbrc 584	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 {cab 2710 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 ∃!wreu 3375 ∃*wrmo 3376 {crab 3433 ⦋csb 3894 ∖ cdif 3946 ∪ cun 3947 ∩ cin 3948 ⊆ wss 3949 ∅c0 4323 ifcif 4529 {csn 4629 class class class wbr 5149 ↦ cmpt 5232 × cxp 5675 ran crn 5678 “ cima 5680 ⟶wf 6540 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 ∘_f cof 7668 1^st c1st 7973 2^nd c2nd 7974 ↑_m cmap 8820 ℂcc 11108 0cc0 11110 1c1 11111 + caddc 11113 < clt 11248 − cmin 11444 ℕcn 12212 ℕ₀cn0 12472 ℤcz 12558 ℤ_≥cuz 12822 ...cfz 13484 ..^cfzo 13627

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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7670 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-n0 12473 df-z 12559 df-uz 12823 df-fz 13485 df-fzo 13628

This theorem is referenced by: poimirlem22 36510

W3C validator