poimirlem9 - Mathbox for Brendan Leahy

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

Theorem poimirlem9 34348

Description: Lemma for poimir 34372, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (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(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem9.1	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem9.2	⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
poimirlem9.3	⊢ (𝜑 → 𝑈 ∈ 𝑆)
poimirlem9.4	⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ≠ (2^nd ‘(1^st ‘𝑇)))

**Assertion**
Ref	Expression
poimirlem9	⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))

Distinct variable groups: 𝑓,𝑗,𝑡,𝑦 𝜑,𝑗,𝑦 𝑗,𝐹,𝑦 𝑗,𝑁,𝑦 𝑇,𝑗,𝑦 𝑈,𝑗,𝑦 𝜑,𝑡 𝑓,𝐾,𝑗,𝑡 𝑓,𝑁,𝑡 𝑇,𝑓 𝑈,𝑓 𝑓,𝐹,𝑡 𝑡,𝑇 𝑡,𝑈 𝑆,𝑗,𝑡,𝑦 Allowed substitution hints: 𝜑(𝑓) 𝑆(𝑓) 𝐾(𝑦)

**Proof of Theorem poimirlem9**
Step	Hyp	Ref	Expression
1		resundi 5712	. . . 4 ⊢ ((2^nd ‘(1^st ‘𝑈)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
2		poimir.0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 11457	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4		npcan1 10866	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
5	3, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
6	2	nnzd 11899	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
7		peano2zm 11838	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8		uzid 12073	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
9		peano2uz 12115	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
10	6, 7, 8, 9	4syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
11	5, 10	eqeltrrd 2867	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
12		fzss2 12763	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14		poimirlem9.2	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
15	13, 14	sseldd 3859	. . . . . . . 8 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...𝑁))
16		fzp1elp1 12776	. . . . . . . . . 10 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
17	14, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
18	5	oveq2d 6992	. . . . . . . . 9 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
19	17, 18	eleqtrd 2868	. . . . . . . 8 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
20	15, 19	prssd 4629	. . . . . . 7 ⊢ (𝜑 → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
21		undif 4313	. . . . . . 7 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
22	20, 21	sylib 210	. . . . . 6 ⊢ (𝜑 → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
23	22	reseq2d 5695	. . . . 5 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑈)) ↾ (1...𝑁)))
24		poimirlem9.3	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
25		elrabi 3590	. . . . . . . . 9 ⊢ (𝑈 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
26		poimirlem22.s	. . . . . . . . 9 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
27	25, 26	eleq2s 2884	. . . . . . . 8 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28		xp1st 7533	. . . . . . . 8 ⊢ (𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29		xp2nd 7534	. . . . . . . 8 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
30	24, 27, 28, 29	4syl 19	. . . . . . 7 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
31		fvex 6512	. . . . . . . 8 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
32		f1oeq1 6433	. . . . . . . 8 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
33	31, 32	elab 3582	. . . . . . 7 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
34	30, 33	sylib 210	. . . . . 6 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
35		f1ofn 6445	. . . . . 6 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)) Fn (1...𝑁))
36		fnresdm 6299	. . . . . 6 ⊢ ((2^nd ‘(1^st ‘𝑈)) Fn (1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) ↾ (1...𝑁)) = (2^nd ‘(1^st ‘𝑈)))
37	34, 35, 36	3syl 18	. . . . 5 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ (1...𝑁)) = (2^nd ‘(1^st ‘𝑈)))
38	23, 37	eqtrd 2814	. . . 4 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (2^nd ‘(1^st ‘𝑈)))
39	1, 38	syl5eqr 2828	. . 3 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (2^nd ‘(1^st ‘𝑈)))
40		2lt3 11619	. . . . . 6 ⊢ 2 < 3
41		2re 11514	. . . . . . 7 ⊢ 2 ∈ ℝ
42		3re 11520	. . . . . . 7 ⊢ 3 ∈ ℝ
43	41, 42	ltnlei 10561	. . . . . 6 ⊢ (2 < 3 ↔ ¬ 3 ≤ 2)
44	40, 43	mpbi 222	. . . . 5 ⊢ ¬ 3 ≤ 2
45		df-pr 4444	. . . . . . . . . . . 12 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩} ∪ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
46	45	coeq2i 5581	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩} ∪ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
47		coundi 5939	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩} ∪ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) = (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
48	46, 47	eqtri 2802	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) = (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
49		poimirlem9.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
50		elrabi 3590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
51	50, 26	eleq2s 2884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52		xp1st 7533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53		xp2nd 7534	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
54	49, 51, 52, 53	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
55		fvex 6512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
56		f1oeq1 6433	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
57	55, 56	elab 3582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
58	54, 57	sylib 210	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
59		f1of1 6443	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
61	19	snssd 4616	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
62		f1ores 6458	. . . . . . . . . . . . . . . . 17 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
63	60, 61, 62	syl2anc 576	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
64		f1of 6444	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}) → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
66		f1ofn 6445	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
67	58, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
68		fnsnfv 6571	. . . . . . . . . . . . . . . . 17 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} = ((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
69	67, 19, 68	syl2anc 576	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} = ((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)}))
70	69	feq3d 6331	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} ↔ ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1)})))
71	65, 70	mpbird 249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
72		eqid 2778	. . . . . . . . . . . . . . 15 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩} = {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}
73		fvex 6512	. . . . . . . . . . . . . . . 16 ⊢ (2^nd ‘𝑇) ∈ V
74		ovex 7008	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
75	73, 74	fsn 6720	. . . . . . . . . . . . . . 15 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}:{(2^nd ‘𝑇)}⟶{((2^nd ‘𝑇) + 1)} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩} = {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩})
76	72, 75	mpbir 223	. . . . . . . . . . . . . 14 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}:{(2^nd ‘𝑇)}⟶{((2^nd ‘𝑇) + 1)}
77		fco2 6362	. . . . . . . . . . . . . 14 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}):{((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}:{(2^nd ‘𝑇)}⟶{((2^nd ‘𝑇) + 1)}) → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}):{(2^nd ‘𝑇)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
78	71, 76, 77	sylancl 577	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}):{(2^nd ‘𝑇)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
79		fvex 6512	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ∈ V
80	79	fconst2 6794	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}):{(2^nd ‘𝑇)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) = ({(2^nd ‘𝑇)} × {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))}))
81	78, 80	sylib 210	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) = ({(2^nd ‘𝑇)} × {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))}))
82	73, 79	xpsn 6726	. . . . . . . . . . . 12 ⊢ ({(2^nd ‘𝑇)} × {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))}) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}
83	81, 82	syl6eq 2830	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
84	83	uneq1d 4027	. . . . . . . . . 10 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) = ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})))
85	48, 84	syl5eq 2826	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) = ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})))
86		elfznn 12752	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
87	14, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
88	87	nnred 11456	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
89	88	ltp1d 11371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
90	88, 89	ltned 10576	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
91	90	necomd 3022	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇))
92		f1veqaeq 6840	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2^nd ‘𝑇) ∈ (1...𝑁))) → (((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) = ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) = (2^nd ‘𝑇)))
93	60, 19, 15, 92	syl12anc 824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) = ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) = (2^nd ‘𝑇)))
94	93	necon3d 2988	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇) → ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ≠ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))))
95	91, 94	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ≠ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)))
96	95	neneqd 2972	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) = ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)))
97	73, 79	opth 5225	. . . . . . . . . . . 12 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ↔ ((2^nd ‘𝑇) = (2^nd ‘𝑇) ∧ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) = ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))))
98	97	simprbi 489	. . . . . . . . . . 11 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ → ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) = ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)))
99	96, 98	nsyl 138	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩)
100	90	neneqd 2972	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1))
101	73, 79	opth1 5224	. . . . . . . . . . 11 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1))
102	100, 101	nsyl 138	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩)
103		opex 5213	. . . . . . . . . . . . . . 15 ⊢ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ V
104	103	snid 4473	. . . . . . . . . . . . . 14 ⊢ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}
105		elun1 4041	. . . . . . . . . . . . . 14 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} → ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})))
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
107		eleq2 2854	. . . . . . . . . . . . 13 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} → (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) ↔ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}))
108	106, 107	mpbii 225	. . . . . . . . . . . 12 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} → ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
109	103	elpr 4464	. . . . . . . . . . . . 13 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ↔ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∨ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩))
110		oran 972	. . . . . . . . . . . . 13 ⊢ ((⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∨ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩) ↔ ¬ (¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∧ ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩))
111	109, 110	bitri 267	. . . . . . . . . . . 12 ⊢ (⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ ∈ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ↔ ¬ (¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∧ ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩))
112	108, 111	sylib 210	. . . . . . . . . . 11 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} → ¬ (¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∧ ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩))
113	112	necon2ai 2996	. . . . . . . . . 10 ⊢ ((¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩ ∧ ¬ ⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩ = ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩) → ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
114	99, 102, 113	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
115	85, 114	eqnetrd 3034	. . . . . . . 8 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
116		fnressn 6743	. . . . . . . . . . . 12 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ (2^nd ‘𝑇) ∈ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇)}) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩})
117	67, 15, 116	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇)}) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩})
118		fnressn 6743	. . . . . . . . . . . 12 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}) = {⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
119	67, 19, 118	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}) = {⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
120	117, 119	uneq12d 4029	. . . . . . . . . 10 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)})) = ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩} ∪ {⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}))
121		df-pr 4444	. . . . . . . . . . . 12 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} = ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})
122	121	reseq2i 5692	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ↾ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
123		resundi 5712	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑇)) ↾ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}))
124	122, 123	eqtri 2802	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1)}))
125		df-pr 4444	. . . . . . . . . 10 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} = ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩} ∪ {⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
126	120, 124, 125	3eqtr4g 2839	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩})
127		poimirlem9.4	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ≠ (2^nd ‘(1^st ‘𝑇)))
128	2, 26, 49, 14, 24	poimirlem8 34347	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
129		uneq12 4023	. . . . . . . . . . . . . 14 ⊢ ((((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
130		resundi 5712	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
131	22	reseq2d 5695	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑇)) ↾ (1...𝑁)))
132		fnresdm 6299	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) ↾ (1...𝑁)) = (2^nd ‘(1^st ‘𝑇)))
133	58, 66, 132	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ (1...𝑁)) = (2^nd ‘(1^st ‘𝑇)))
134	131, 133	eqtrd 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (2^nd ‘(1^st ‘𝑇)))
135	130, 134	syl5eqr 2828	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (2^nd ‘(1^st ‘𝑇)))
136	39, 135	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) ↔ (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘(1^st ‘𝑇))))
137	129, 136	syl5ib 236	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘(1^st ‘𝑇))))
138	128, 137	mpan2d 681	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘(1^st ‘𝑇))))
139	138	necon3d 2988	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ≠ (2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
140	127, 139	mpd 15	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
141	140	necomd 3022	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
142	126, 141	eqnetrrd 3035	. . . . . . . 8 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
143		prex 5189	. . . . . . . . . . . 12 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∈ V
144	55, 143	coex 7450	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ∈ V
145		prex 5189	. . . . . . . . . . 11 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∈ V
146	31	resex 5744	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V
147		hashtpg 13654	. . . . . . . . . . 11 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ∈ V ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∈ V ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V) → ((((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) ↔ (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3))
148	144, 145, 146, 147	mp3an 1440	. . . . . . . . . 10 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) ↔ (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3)
149	148	biimpi 208	. . . . . . . . 9 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})) → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3)
150	149	3expia 1101	. . . . . . . 8 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ≠ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} ≠ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3))
151	115, 142, 150	syl2anc 576	. . . . . . 7 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3))
152		prex 5189	. . . . . . . . . . . . 13 ⊢ {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∈ V
153		prex 5189	. . . . . . . . . . . . 13 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ V
154	152, 153	mapval 8218	. . . . . . . . . . . 12 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}
155		prfi 8588	. . . . . . . . . . . . 13 ⊢ {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∈ Fin
156		prfi 8588	. . . . . . . . . . . . 13 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin
157		mapfi 8615	. . . . . . . . . . . . 13 ⊢ (({((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∈ Fin ∧ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin) → ({((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ Fin)
158	155, 156, 157	mp2an 679	. . . . . . . . . . . 12 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ Fin
159	154, 158	eqeltrri 2863	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin
160		f1of 6444	. . . . . . . . . . . 12 ⊢ (𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} → 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
161	160	ss2abi 3933	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}
162		ssfi 8533	. . . . . . . . . . 11 ⊢ (({𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) → {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin)
163	159, 161, 162	mp2an 679	. . . . . . . . . 10 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin
164	19, 15	prssd 4629	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ⊆ (1...𝑁))
165		f1ores 6458	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ⊆ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}))
166	60, 164, 165	syl2anc 576	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}))
167		fnimapr 6575	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2^nd ‘𝑇) ∈ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
168	67, 19, 15, 167	syl3anc 1351	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
169	168	f1oeq3d 6441	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→((2^nd ‘(1^st ‘𝑇)) “ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ↔ ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
170	166, 169	mpbid 224	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
171		f1oprg 6488	. . . . . . . . . . . . . . 15 ⊢ ((((2^nd ‘𝑇) ∈ V ∧ ((2^nd ‘𝑇) + 1) ∈ V) ∧ (((2^nd ‘𝑇) + 1) ∈ V ∧ (2^nd ‘𝑇) ∈ V)) → (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}))
172	73, 74, 74, 73, 171	mp4an 680	. . . . . . . . . . . . . 14 ⊢ (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
173	90, 91, 172	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
174		f1oco 6466	. . . . . . . . . . . . 13 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}):{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) → (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
175	170, 173, 174	syl2anc 576	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
176		rnpropg 5918	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘𝑇) ∈ V ∧ ((2^nd ‘𝑇) + 1) ∈ V) → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
177	73, 74, 176	mp2an 679	. . . . . . . . . . . . . 14 ⊢ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}
178	177	eqimssi 3915	. . . . . . . . . . . . 13 ⊢ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ⊆ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}
179		cores 5941	. . . . . . . . . . . . 13 ⊢ (ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ⊆ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → (((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) = ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
180		f1oeq1 6433	. . . . . . . . . . . . 13 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) = ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) → ((((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
181	178, 179, 180	mp2b 10	. . . . . . . . . . . 12 ⊢ ((((2^nd ‘(1^st ‘𝑇)) ↾ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
182	175, 181	sylib 210	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
183	95	necomd 3022	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)))
184		fvex 6512	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ∈ V
185		f1oprg 6488	. . . . . . . . . . . . . 14 ⊢ ((((2^nd ‘𝑇) ∈ V ∧ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ∈ V) ∧ (((2^nd ‘𝑇) + 1) ∈ V ∧ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ∈ V)) → (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))) → {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))}))
186	73, 184, 74, 79, 185	mp4an 680	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))) → {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
187	90, 183, 186	syl2anc 576	. . . . . . . . . . . 12 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
188		prcom 4542	. . . . . . . . . . . . 13 ⊢ {((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}
189		f1oeq3 6435	. . . . . . . . . . . . 13 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} → ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
190	188, 189	ax-mp 5	. . . . . . . . . . . 12 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
191	187, 190	sylib 210	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
192		f1of1 6443	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁))
193	34, 192	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁))
194		f1ores 6458	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁) ∧ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑈)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
195	193, 20, 194	syl2anc 576	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑈)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
196		dff1o3 6450	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑈))))
197	196	simprbi 489	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
198		imadif 6271	. . . . . . . . . . . . . . . 16 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
199	34, 197, 198	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
200		f1ofo 6451	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
201		foima 6424	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
202	34, 200, 201	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
203		f1ofo 6451	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
204		foima 6424	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
205	58, 203, 204	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
206	202, 205	eqtr4d 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)))
207	128	rneqd 5651	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ran ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
208		df-ima 5420	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ran ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
209		df-ima 5420	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ran ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
210	207, 208, 209	3eqtr4g 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
211	206, 210	difeq12d 3990	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
212		dff1o3 6450	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
213	212	simprbi 489	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
214		imadif 6271	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
215	58, 213, 214	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
216		dfin4 4131	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
217		sseqin2 4079	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
218	20, 217	sylib 210	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
219	216, 218	syl5eqr 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
220	219	imaeq2d 5770	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
221	215, 220	eqtr3d 2816	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
222	199, 211, 221	3eqtrd 2818	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
223	219	imaeq2d 5770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑈)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
224		fnimapr 6575	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ (2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
225	67, 15, 19, 224	syl3anc 1351	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))})
226	225, 188	syl6eq 2830	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
227	222, 223, 226	3eqtr3d 2822	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
228	227	f1oeq3d 6441	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→((2^nd ‘(1^st ‘𝑈)) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ↔ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
229	195, 228	mpbid 224	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
230		ssabral 3932	. . . . . . . . . . . 12 ⊢ ({((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ↔ ∀𝑓 ∈ {((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))})
231		f1oeq1 6433	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) → (𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
232		f1oeq1 6433	. . . . . . . . . . . . 13 ⊢ (𝑓 = {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩} → (𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
233		f1oeq1 6433	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
234	144, 145, 146, 231, 232, 233	raltp 4515	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ {((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ↔ (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
235	230, 234	bitri 267	. . . . . . . . . . 11 ⊢ ({((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ↔ (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∧ {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∧ ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}):{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}))
236	182, 191, 229, 235	syl3anbrc 1323	. . . . . . . . . 10 ⊢ (𝜑 → {((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}})
237		hashss 13583	. . . . . . . . . 10 ⊢ (({𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin ∧ {((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) ≤ (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}))
238	163, 236, 237	sylancr 578	. . . . . . . . 9 ⊢ (𝜑 → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) ≤ (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}))
239	153	enref 8339	. . . . . . . . . . . 12 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
240		hashprg 13569	. . . . . . . . . . . . . . . 16 ⊢ ((((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ∈ V ∧ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ∈ V) → (((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ≠ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ↔ (♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = 2))
241	79, 184, 240	mp2an 679	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) ≠ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) ↔ (♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = 2)
242	95, 241	sylib 210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = 2)
243		hashprg 13569	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘𝑇) ∈ V ∧ ((2^nd ‘𝑇) + 1) ∈ V) → ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ↔ (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = 2))
244	73, 74, 243	mp2an 679	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ↔ (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = 2)
245	90, 244	sylib 210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = 2)
246	242, 245	eqtr4d 2817	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
247		hashen 13522	. . . . . . . . . . . . . 14 ⊢ (({((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ∈ Fin ∧ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin) → ((♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ↔ {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
248	155, 156, 247	mp2an 679	. . . . . . . . . . . . 13 ⊢ ((♯‘{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}) = (♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ↔ {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
249	246, 248	sylib 210	. . . . . . . . . . . 12 ⊢ (𝜑 → {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
250		hashfacen 13625	. . . . . . . . . . . 12 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ {((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))} ≈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}})
251	239, 249, 250	sylancr 578	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}})
252	153, 153	mapval 8218	. . . . . . . . . . . . . 14 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}
253		mapfi 8615	. . . . . . . . . . . . . . 15 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin ∧ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ Fin)
254	156, 156, 253	mp2an 679	. . . . . . . . . . . . . 14 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ↑_𝑚 {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ Fin
255	252, 254	eqeltrri 2863	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ∈ Fin
256		f1of 6444	. . . . . . . . . . . . . 14 ⊢ (𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
257	256	ss2abi 3933	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}
258		ssfi 8533	. . . . . . . . . . . . 13 ⊢ (({𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) → {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ∈ Fin)
259	255, 257, 258	mp2an 679	. . . . . . . . . . . 12 ⊢ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ∈ Fin
260		hashen 13522	. . . . . . . . . . . 12 ⊢ (({𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}} ∈ Fin) → ((♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}))
261	163, 259, 260	mp2an 679	. . . . . . . . . . 11 ⊢ ((♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}})
262	251, 261	sylibr 226	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}))
263		hashfac 13629	. . . . . . . . . . . 12 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∈ Fin → (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) = (!‘(♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
264	156, 263	ax-mp 5	. . . . . . . . . . 11 ⊢ (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) = (!‘(♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
265	245	fveq2d 6503	. . . . . . . . . . . 12 ⊢ (𝜑 → (!‘(♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (!‘2))
266		fac2 13454	. . . . . . . . . . . 12 ⊢ (!‘2) = 2
267	265, 266	syl6eq 2830	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘(♯‘{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = 2)
268	264, 267	syl5eq 2826	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}}) = 2)
269	262, 268	eqtrd 2814	. . . . . . . . 9 ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))}}) = 2)
270	238, 269	breqtrd 4955	. . . . . . . 8 ⊢ (𝜑 → (♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) ≤ 2)
271		breq1 4932	. . . . . . . 8 ⊢ ((♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3 → ((♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) ≤ 2 ↔ 3 ≤ 2))
272	270, 271	syl5ibcom 237	. . . . . . 7 ⊢ (𝜑 → ((♯‘{((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}), {⟨(2^nd ‘𝑇), ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇))⟩, ⟨((2^nd ‘𝑇) + 1), ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))⟩}, ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})}) = 3 → 3 ≤ 2))
273	151, 272	syld 47	. . . . . 6 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) → 3 ≤ 2))
274	273	necon1bd 2985	. . . . 5 ⊢ (𝜑 → (¬ 3 ≤ 2 → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})))
275	44, 274	mpi 20	. . . 4 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}))
276		coires1 5956	. . . . 5 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((2^nd ‘(1^st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
277	128, 276	syl6eqr 2832	. . . 4 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((2^nd ‘(1^st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
278	275, 277	uneq12d 4029	. . 3 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) ↾ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ((2^nd ‘(1^st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
279	39, 278	eqtr3d 2816	. 2 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) = (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
280		coundi 5939	. 2 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) = (((2^nd ‘(1^st ‘𝑇)) ∘ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}) ∪ ((2^nd ‘(1^st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))
281	279, 280	syl6eqr 2832	1 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∨ wo 833 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 {cab 2758 ≠ wne 2967 ∀wral 3088 {crab 3092 Vcvv 3415 ⦋csb 3786 ∖ cdif 3826 ∪ cun 3827 ∩ cin 3828 ⊆ wss 3829 ifcif 4350 {csn 4441 {cpr 4443 {ctp 4445 ⟨cop 4447 class class class wbr 4929 ↦ cmpt 5008 I cid 5311 × cxp 5405 ^◡ccnv 5406 ran crn 5408 ↾ cres 5409 “ cima 5410 ∘ ccom 5411 Fun wfun 6182 Fn wfn 6183 ⟶wf 6184 –1-1→wf1 6185 –onto→wfo 6186 –1-1-onto→wf1o 6187 ‘cfv 6188 (class class class)co 6976 ∘_𝑓 cof 7225 1^st c1st 7499 2^nd c2nd 7500 ↑_𝑚 cmap 8206 ≈ cen 8303 Fincfn 8306 ℂcc 10333 0cc0 10335 1c1 10336 + caddc 10338 < clt 10474 ≤ cle 10475 − cmin 10670 ℕcn 11439 2c2 11495 3c3 11496 ℤcz 11793 ℤ_≥cuz 12058 ...cfz 12708 ..^cfzo 12849 !cfa 13448 ♯chash 13505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5049 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-int 4750 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-of 7227 df-om 7397 df-1st 7501 df-2nd 7502 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-1o 7905 df-2o 7906 df-oadd 7909 df-er 8089 df-map 8208 df-pm 8209 df-en 8307 df-dom 8308 df-sdom 8309 df-fin 8310 df-dju 9124 df-card 9162 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-div 11099 df-nn 11440 df-2 11503 df-3 11504 df-n0 11708 df-xnn0 11780 df-z 11794 df-uz 12059 df-fz 12709 df-fzo 12850 df-seq 13185 df-fac 13449 df-bc 13478 df-hash 13506

This theorem is referenced by: poimirlem22 34361

W3C validator