poimirlem15

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
	poimirlem22.2	$⊢ φ \to T \in S$
	poimirlem15.3	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
Assertion	poimirlem15	$⊢ φ \to ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in S$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
4		poimirlem22.2	$⊢ φ \to T \in S$
5		poimirlem15.3	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
6		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
7	6 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
8	4 7	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
9		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
10		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
11	8 9 10	3syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
12		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
13	8 9 12	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
14		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
15		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
16	14 15	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
17	13 16	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
18		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
19	5 18	syl	$⊢ φ \to 2^{nd} (T) \in ℕ$
20	19	nnred	$⊢ φ \to 2^{nd} (T) \in ℝ$
21	20	ltp1d	$⊢ φ \to 2^{nd} (T) < 2^{nd} (T) + 1$
22	20 21	ltned	$⊢ φ \to 2^{nd} (T) \neq 2^{nd} (T) + 1$
23	22	necomd	$⊢ φ \to 2^{nd} (T) + 1 \neq 2^{nd} (T)$
24		fvex	$⊢ 2^{nd} (T) \in V$
25		ovex	$⊢ 2^{nd} (T) + 1 \in V$
26		f1oprg	$⊢ ((2^{nd} (T) \in V \land 2^{nd} (T) + 1 \in V) \land (2^{nd} (T) + 1 \in V \land 2^{nd} (T) \in V)) \to ((2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \neq 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\})$
27	24 25 25 24 26	mp4an	$⊢ (2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \neq 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}$
28	22 23 27	syl2anc	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}$
29		prcom	$⊢ \{2^{nd} (T) + 1, 2^{nd} (T)\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
30		f1oeq3	$⊢ \{2^{nd} (T) + 1, 2^{nd} (T)\} = \{2^{nd} (T), 2^{nd} (T) + 1\} \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\})$
31	29 30	ax-mp	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}$
32	28 31	sylib	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}$
33		f1oi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
34		disjdif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset$
35		f1oun	$⊢ ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \land ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \land (\{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset \land \{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset)) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
36	34 34 35	mpanr12	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \land ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
37	32 33 36	sylancl	$⊢ φ \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
38	1	nncnd	$⊢ φ \to N \in ℂ$
39		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
40	38 39	syl	$⊢ φ \to N - 1 + 1 = N$
41	1	nnzd	$⊢ φ \to N \in ℤ$
42		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
43	41 42	syl	$⊢ φ \to N - 1 \in ℤ$
44		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
45		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
46	43 44 45	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
47	40 46	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
48		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
49	47 48	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
50	49 5	sseldd	$⊢ φ \to 2^{nd} (T) \in (1 \dots N)$
51	19	peano2nnd	$⊢ φ \to 2^{nd} (T) + 1 \in ℕ$
52	43	zred	$⊢ φ \to N - 1 \in ℝ$
53	1	nnred	$⊢ φ \to N \in ℝ$
54		elfzle2	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \leq N - 1$
55	5 54	syl	$⊢ φ \to 2^{nd} (T) \leq N - 1$
56	53	ltm1d	$⊢ φ \to N - 1 < N$
57	20 52 53 55 56	lelttrd	$⊢ φ \to 2^{nd} (T) < N$
58	19	nnzd	$⊢ φ \to 2^{nd} (T) \in ℤ$
59		zltp1le	$⊢ (2^{nd} (T) \in ℤ \land N \in ℤ) \to (2^{nd} (T) < N \leftrightarrow 2^{nd} (T) + 1 \leq N)$
60	58 41 59	syl2anc	$⊢ φ \to (2^{nd} (T) < N \leftrightarrow 2^{nd} (T) + 1 \leq N)$
61	57 60	mpbid	$⊢ φ \to 2^{nd} (T) + 1 \leq N$
62		fznn	$⊢ N \in ℤ \to (2^{nd} (T) + 1 \in (1 \dots N) \leftrightarrow (2^{nd} (T) + 1 \in ℕ \land 2^{nd} (T) + 1 \leq N))$
63	41 62	syl	$⊢ φ \to (2^{nd} (T) + 1 \in (1 \dots N) \leftrightarrow (2^{nd} (T) + 1 \in ℕ \land 2^{nd} (T) + 1 \leq N))$
64	51 61 63	mpbir2and	$⊢ φ \to 2^{nd} (T) + 1 \in (1 \dots N)$
65		prssi	$⊢ (2^{nd} (T) \in (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)$
66	50 64 65	syl2anc	$⊢ φ \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)$
67		undif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) \leftrightarrow \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N)$
68	66 67	sylib	$⊢ φ \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N)$
69		f1oeq23	$⊢ (\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N) \land \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N)) \to ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \leftrightarrow (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
70	68 68 69	syl2anc	$⊢ φ \to ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \leftrightarrow (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
71	37 70	mpbid	$⊢ φ \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
72		f1oco	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
73	17 71 72	syl2anc	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
74		prex	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \in V$
75		ovex	$⊢ (1 \dots N) \in V$
76		difexg	$⊢ (1 \dots N) \in V \to (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \in V$
77		resiexg	$⊢ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \in V \to {I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} \in V$
78	75 76 77	mp2b	$⊢ {I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} \in V$
79	74 78	unex	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) \in V$
80	14 79	coex	$⊢ 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \in V$
81		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
82	80 81	elab	$⊢ 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
83	73 82	sylibr	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
84		opelxpi	$⊢ (1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \land 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
85	11 83 84	syl2anc	$⊢ φ \to ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
86		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
87	49 86	sstrdi	$⊢ φ \to (1 \dots N - 1) \subseteq (0 \dots N)$
88	87 5	sseldd	$⊢ φ \to 2^{nd} (T) \in (0 \dots N)$
89		opelxpi	$⊢ (⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land 2^{nd} (T) \in (0 \dots N)) \to ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
90	85 88 89	syl2anc	$⊢ φ \to ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
91		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
92	91	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
93	92	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
94	93	csbeq1d	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))$
95		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
96		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
97	96	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
98	97	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
99	96	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
100	99	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
101	98 100	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
102	95 101	oveq12d	$⊢ t = T \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))$
103	102	csbeq2dv	$⊢ t = T \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
104	94 103	eqtrd	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
105	104	mpteq2dv	$⊢ t = T \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
106	105	eqeq2d	$⊢ t = T \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
107	106 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
108	107	simprbi	$⊢ T \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
109	4 108	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
110		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] = 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y)]]$
111		f1ofn	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\} \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\}$
112	28 111	syl	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\}$
113	112	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\}$
114		incom	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (1 \dots y) = (1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\}$
115		elfznn0	$⊢ y \in (0 \dots N - 1) \to y \in ℕ_{0}$
116	115	nn0red	$⊢ y \in (0 \dots N - 1) \to y \in ℝ$
117		ltnle	$⊢ (y \in ℝ \land 2^{nd} (T) \in ℝ) \to (y < 2^{nd} (T) \leftrightarrow \neg 2^{nd} (T) \leq y)$
118	116 20 117	syl2anr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y < 2^{nd} (T) \leftrightarrow \neg 2^{nd} (T) \leq y)$
119	118	biimpa	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \neg 2^{nd} (T) \leq y$
120		elfzle2	$⊢ 2^{nd} (T) \in (1 \dots y) \to 2^{nd} (T) \leq y$
121	119 120	nsyl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \neg 2^{nd} (T) \in (1 \dots y)$
122		disjsn	$⊢ (1 \dots y) \cap \{2^{nd} (T)\} = \emptyset \leftrightarrow \neg 2^{nd} (T) \in (1 \dots y)$
123	121 122	sylibr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (1 \dots y) \cap \{2^{nd} (T)\} = \emptyset$
124	116	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y \in ℝ$
125	20	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) \in ℝ$
126	51	nnred	$⊢ φ \to 2^{nd} (T) + 1 \in ℝ$
127	126	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) + 1 \in ℝ$
128		simpr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y < 2^{nd} (T)$
129	21	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) < 2^{nd} (T) + 1$
130	124 125 127 128 129	lttrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y < 2^{nd} (T) + 1$
131		ltnle	$⊢ (y \in ℝ \land 2^{nd} (T) + 1 \in ℝ) \to (y < 2^{nd} (T) + 1 \leftrightarrow \neg 2^{nd} (T) + 1 \leq y)$
132	116 126 131	syl2anr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y < 2^{nd} (T) + 1 \leftrightarrow \neg 2^{nd} (T) + 1 \leq y)$
133	132	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (y < 2^{nd} (T) + 1 \leftrightarrow \neg 2^{nd} (T) + 1 \leq y)$
134	130 133	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \neg 2^{nd} (T) + 1 \leq y$
135		elfzle2	$⊢ 2^{nd} (T) + 1 \in (1 \dots y) \to 2^{nd} (T) + 1 \leq y$
136	134 135	nsyl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \neg 2^{nd} (T) + 1 \in (1 \dots y)$
137		disjsn	$⊢ (1 \dots y) \cap \{2^{nd} (T) + 1\} = \emptyset \leftrightarrow \neg 2^{nd} (T) + 1 \in (1 \dots y)$
138	136 137	sylibr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (1 \dots y) \cap \{2^{nd} (T) + 1\} = \emptyset$
139	123 138	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ((1 \dots y) \cap \{2^{nd} (T)\}) \cup ((1 \dots y) \cap \{2^{nd} (T) + 1\}) = \emptyset \cup \emptyset$
140		df-pr	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} = \{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}$
141	140	ineq2i	$⊢ (1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots y) \cap (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})$
142		indi	$⊢ (1 \dots y) \cap (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}) = ((1 \dots y) \cap \{2^{nd} (T)\}) \cup ((1 \dots y) \cap \{2^{nd} (T) + 1\})$
143	141 142	eqtr2i	$⊢ ((1 \dots y) \cap \{2^{nd} (T)\}) \cup ((1 \dots y) \cap \{2^{nd} (T) + 1\}) = (1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\}$
144		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
145	139 143 144	3eqtr3g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset$
146	114 145	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (1 \dots y) = \emptyset$
147		fnimadisj	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\} \land \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (1 \dots y) = \emptyset) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y)] = \emptyset$
148	113 146 147	syl2anc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y)] = \emptyset$
149	40	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 = N$
150		elfzuz3	$⊢ y \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq y}$
151		peano2uz	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq y}$
152	150 151	syl	$⊢ y \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq y}$
153	152	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq y}$
154	149 153	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq y}$
155		fzss2	$⊢ N \in ℤ_{\geq y} \to (1 \dots y) \subseteq (1 \dots N)$
156		reldisj	$⊢ (1 \dots y) \subseteq (1 \dots N) \to ((1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (1 \dots y) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
157	154 155 156	3syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (1 \dots y) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
158	157	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ((1 \dots y) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (1 \dots y) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
159	145 158	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (1 \dots y) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
160		resiima	$⊢ (1 \dots y) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y)] = (1 \dots y)$
161	159 160	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y)] = (1 \dots y)$
162	148 161	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y)] = \emptyset \cup (1 \dots y)$
163		imaundir	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y)] = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y)]$
164		uncom	$⊢ \emptyset \cup (1 \dots y) = (1 \dots y) \cup \emptyset$
165		un0	$⊢ (1 \dots y) \cup \emptyset = (1 \dots y)$
166	164 165	eqtr2i	$⊢ (1 \dots y) = \emptyset \cup (1 \dots y)$
167	162 163 166	3eqtr4g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y)] = (1 \dots y)$
168	167	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y)]] = 2^{nd} (1^{st} (T)) [(1 \dots y)]$
169	110 168	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] = 2^{nd} (1^{st} (T)) [(1 \dots y)]$
170	169	xpeq1d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}$
171		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 \dots N)]]$
172		imaundir	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 \dots N)] = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N)]$
173		imassrn	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] \subseteq ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
174	173	a1i	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] \subseteq ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
175		fnima	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\} \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
176	28 111 175	3syl	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
177	176	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
178		elfzelz	$⊢ y \in (0 \dots N - 1) \to y \in ℤ$
179		zltp1le	$⊢ (y \in ℤ \land 2^{nd} (T) \in ℤ) \to (y < 2^{nd} (T) \leftrightarrow y + 1 \leq 2^{nd} (T))$
180	178 58 179	syl2anr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y < 2^{nd} (T) \leftrightarrow y + 1 \leq 2^{nd} (T))$
181	180	biimpa	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y + 1 \leq 2^{nd} (T)$
182	20 53 57	ltled	$⊢ φ \to 2^{nd} (T) \leq N$
183	182	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) \leq N$
184	58	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (T) \in ℤ$
185		nn0p1nn	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ$
186	115 185	syl	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℕ$
187	186	nnzd	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℤ$
188	187	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y + 1 \in ℤ$
189	41	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ$
190		elfz	$⊢ (2^{nd} (T) \in ℤ \land y + 1 \in ℤ \land N \in ℤ) \to (2^{nd} (T) \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) \land 2^{nd} (T) \leq N))$
191	184 188 189 190	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) \land 2^{nd} (T) \leq N))$
192	191	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (T) \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) \land 2^{nd} (T) \leq N))$
193	181 183 192	mpbir2and	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) \in (y + 1 \dots N)$
194		1red	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 1 \in ℝ$
195		ltle	$⊢ (y \in ℝ \land 2^{nd} (T) \in ℝ) \to (y < 2^{nd} (T) \to y \leq 2^{nd} (T))$
196	116 20 195	syl2anr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y < 2^{nd} (T) \to y \leq 2^{nd} (T))$
197	196	imp	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y \leq 2^{nd} (T)$
198	124 125 194 197	leadd1dd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to y + 1 \leq 2^{nd} (T) + 1$
199	61	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) + 1 \leq N$
200	58	peano2zd	$⊢ φ \to 2^{nd} (T) + 1 \in ℤ$
201	200	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (T) + 1 \in ℤ$
202		elfz	$⊢ (2^{nd} (T) + 1 \in ℤ \land y + 1 \in ℤ \land N \in ℤ) \to (2^{nd} (T) + 1 \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \leq N))$
203	201 188 189 202	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) + 1 \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \leq N))$
204	203	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (T) + 1 \in (y + 1 \dots N) \leftrightarrow (y + 1 \leq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \leq N))$
205	198 199 204	mpbir2and	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (T) + 1 \in (y + 1 \dots N)$
206		prssi	$⊢ (2^{nd} (T) \in (y + 1 \dots N) \land 2^{nd} (T) + 1 \in (y + 1 \dots N)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (y + 1 \dots N)$
207	193 205 206	syl2anc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (y + 1 \dots N)$
208		imass2	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (y + 1 \dots N) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)]$
209	207 208	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)]$
210	177 209	eqsstrrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)]$
211	174 210	eqssd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
212		f1ofo	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\} \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}$
213		forn	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\} \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T) + 1, 2^{nd} (T)\}$
214	28 212 213	3syl	$⊢ φ \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T) + 1, 2^{nd} (T)\}$
215	214 29	eqtrdi	$⊢ φ \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
216	215	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
217	211 216	eqtrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] = \{2^{nd} (T), 2^{nd} (T) + 1\}$
218		undif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (y + 1 \dots N) \leftrightarrow \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (y + 1 \dots N)$
219	207 218	sylib	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (y + 1 \dots N)$
220	219	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N)]$
221		fnresi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
222		disjdifr	$⊢ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset$
223		fnimadisj	$⊢ (({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \land ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset$
224	221 222 223	mp2an	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset$
225	224	a1i	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset$
226		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
227	186 226	eleqtrdi	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℤ_{\geq 1}$
228		fzss1	$⊢ y + 1 \in ℤ_{\geq 1} \to (y + 1 \dots N) \subseteq (1 \dots N)$
229	227 228	syl	$⊢ y \in (0 \dots N - 1) \to (y + 1 \dots N) \subseteq (1 \dots N)$
230	229	ssdifd	$⊢ y \in (0 \dots N - 1) \to (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
231		resiima	$⊢ (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
232	230 231	syl	$⊢ y \in (0 \dots N - 1) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
233	232	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
234	225 233	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
235		imaundi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
236		uncom	$⊢ \emptyset \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup \emptyset$
237		un0	$⊢ ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup \emptyset = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
238	236 237	eqtr2i	$⊢ (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
239	234 235 238	3eqtr4g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
240	220 239	eqtr3d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N)] = (y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
241	217 240	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 \dots N)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 \dots N)] = \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
242	172 241	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 \dots N)] = \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((y + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
243	242 219	eqtrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 \dots N)] = (y + 1 \dots N)$
244	243	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 \dots N)]] = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
245	171 244	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
246	245	xpeq1d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}$
247	170 246	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})$
248	247	oveq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
249		iftrue	$⊢ y < 2^{nd} (T) \to if (y < 2^{nd} (T), y, y + 1) = y$
250	249	csbeq1d	$⊢ y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ y / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))$
251		vex	$⊢ y \in V$
252		oveq2	$⊢ j = y \to (1 \dots j) = (1 \dots y)$
253	252	imaeq2d	$⊢ j = y \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)]$
254	253	xpeq1d	$⊢ j = y \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}$
255		oveq1	$⊢ j = y \to j + 1 = y + 1$
256	255	oveq1d	$⊢ j = y \to (j + 1 \dots N) = (y + 1 \dots N)$
257	256	imaeq2d	$⊢ j = y \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)]$
258	257	xpeq1d	$⊢ j = y \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}$
259	254 258	uneq12d	$⊢ j = y \to ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\})$
260	259	oveq2d	$⊢ j = y \to 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}))$
261	251 260	csbie	$⊢ ⦋ y / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}))$
262	250 261	eqtrdi	$⊢ y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}))$
263	262	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 \dots N)] \times \{0\}))$
264	249	csbeq1d	$⊢ y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ y / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
265	252	imaeq2d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots y)]$
266	265	xpeq1d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}$
267	256	imaeq2d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
268	267	xpeq1d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}$
269	266 268	uneq12d	$⊢ j = y \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})$
270	269	oveq2d	$⊢ j = y \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
271	251 270	csbie	$⊢ ⦋ y / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
272	264 271	eqtrdi	$⊢ y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
273	272	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
274	248 263 273	3eqtr4d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
275		lenlt	$⊢ (2^{nd} (T) \in ℝ \land y \in ℝ) \to (2^{nd} (T) \leq y \leftrightarrow \neg y < 2^{nd} (T))$
276	20 116 275	syl2an	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) \leq y \leftrightarrow \neg y < 2^{nd} (T))$
277	276	biimpar	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to 2^{nd} (T) \leq y$
278		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y + 1)]]$
279		imaundir	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y + 1)] = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1)]$
280		imassrn	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] \subseteq ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
281	280	a1i	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] \subseteq ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
282	176	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
283	19	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) \in ℕ$
284	20	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) \in ℝ$
285	116	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to y \in ℝ$
286	186	nnred	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℝ$
287	286	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to y + 1 \in ℝ$
288		simpr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) \leq y$
289	116	lep1d	$⊢ y \in (0 \dots N - 1) \to y \leq y + 1$
290	289	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to y \leq y + 1$
291	284 285 287 288 290	letrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) \leq y + 1$
292		fznn	$⊢ y + 1 \in ℤ \to (2^{nd} (T) \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) \in ℕ \land 2^{nd} (T) \leq y + 1))$
293	187 292	syl	$⊢ y \in (0 \dots N - 1) \to (2^{nd} (T) \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) \in ℕ \land 2^{nd} (T) \leq y + 1))$
294	293	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (T) \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) \in ℕ \land 2^{nd} (T) \leq y + 1))$
295	283 291 294	mpbir2and	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) \in (1 \dots y + 1)$
296	51	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) + 1 \in ℕ$
297		1red	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 1 \in ℝ$
298	284 285 297 288	leadd1dd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) + 1 \leq y + 1$
299		fznn	$⊢ y + 1 \in ℤ \to (2^{nd} (T) + 1 \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) + 1 \in ℕ \land 2^{nd} (T) + 1 \leq y + 1))$
300	187 299	syl	$⊢ y \in (0 \dots N - 1) \to (2^{nd} (T) + 1 \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) + 1 \in ℕ \land 2^{nd} (T) + 1 \leq y + 1))$
301	300	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (T) + 1 \in (1 \dots y + 1) \leftrightarrow (2^{nd} (T) + 1 \in ℕ \land 2^{nd} (T) + 1 \leq y + 1))$
302	296 298 301	mpbir2and	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) + 1 \in (1 \dots y + 1)$
303		prssi	$⊢ (2^{nd} (T) \in (1 \dots y + 1) \land 2^{nd} (T) + 1 \in (1 \dots y + 1)) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots y + 1)$
304	295 302 303	syl2anc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots y + 1)$
305		imass2	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots y + 1) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)]$
306	304 305	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [\{2^{nd} (T), 2^{nd} (T) + 1\}] \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)]$
307	282 306	eqsstrrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \subseteq \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)]$
308	281 307	eqssd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] = ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
309	215	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
310	308 309	eqtrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] = \{2^{nd} (T), 2^{nd} (T) + 1\}$
311		undif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots y + 1) \leftrightarrow \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots y + 1)$
312	304 311	sylib	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots y + 1)$
313	312	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1)]$
314	224	a1i	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset$
315		eluzp1p1	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
316	150 315	syl	$⊢ y \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
317	316	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
318	149 317	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq (y + 1)}$
319		fzss2	$⊢ N \in ℤ_{\geq (y + 1)} \to (1 \dots y + 1) \subseteq (1 \dots N)$
320	318 319	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots y + 1) \subseteq (1 \dots N)$
321	320	ssdifd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
322	321	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
323		resiima	$⊢ (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
324	322 323	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
325	314 324	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = \emptyset \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
326		imaundi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\}] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
327		uncom	$⊢ \emptyset \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup \emptyset$
328		un0	$⊢ ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup \emptyset = (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
329	327 328	eqtr2i	$⊢ (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
330	325 326 329	3eqtr4g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
331	313 330	eqtr3d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1)] = (1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
332	310 331	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(1 \dots y + 1)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(1 \dots y + 1)] = \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
333	279 332	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y + 1)] = \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots y + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
334	333 312	eqtrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y + 1)] = (1 \dots y + 1)$
335	334	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(1 \dots y + 1)]] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
336	278 335	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
337	336	xpeq1d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}$
338		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 + 1 \dots N)]]$
339	112	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\}$
340		incom	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (y + 1 + 1 \dots N) = (y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\}$
341	126	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) + 1 \in ℝ$
342	186	peano2nnd	$⊢ y \in (0 \dots N - 1) \to y + 1 + 1 \in ℕ$
343	342	nnred	$⊢ y \in (0 \dots N - 1) \to y + 1 + 1 \in ℝ$
344	343	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to y + 1 + 1 \in ℝ$
345	21	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) < 2^{nd} (T) + 1$
346	116	ltp1d	$⊢ y \in (0 \dots N - 1) \to y < y + 1$
347	346	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to y < y + 1$
348	284 285 287 288 347	lelttrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) < y + 1$
349	284 287 297 348	ltadd1dd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) + 1 < y + 1 + 1$
350	284 341 344 345 349	lttrd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (T) < y + 1 + 1$
351		ltnle	$⊢ (2^{nd} (T) \in ℝ \land y + 1 + 1 \in ℝ) \to (2^{nd} (T) < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T))$
352	20 343 351	syl2an	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T))$
353	352	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (T) < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T))$
354	350 353	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \neg y + 1 + 1 \leq 2^{nd} (T)$
355		elfzle1	$⊢ 2^{nd} (T) \in (y + 1 + 1 \dots N) \to y + 1 + 1 \leq 2^{nd} (T)$
356	354 355	nsyl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \neg 2^{nd} (T) \in (y + 1 + 1 \dots N)$
357		disjsn	$⊢ (y + 1 + 1 \dots N) \cap \{2^{nd} (T)\} = \emptyset \leftrightarrow \neg 2^{nd} (T) \in (y + 1 + 1 \dots N)$
358	356 357	sylibr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (y + 1 + 1 \dots N) \cap \{2^{nd} (T)\} = \emptyset$
359		ltnle	$⊢ (2^{nd} (T) + 1 \in ℝ \land y + 1 + 1 \in ℝ) \to (2^{nd} (T) + 1 < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T) + 1)$
360	126 343 359	syl2an	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) + 1 < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T) + 1)$
361	360	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (T) + 1 < y + 1 + 1 \leftrightarrow \neg y + 1 + 1 \leq 2^{nd} (T) + 1)$
362	349 361	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \neg y + 1 + 1 \leq 2^{nd} (T) + 1$
363		elfzle1	$⊢ 2^{nd} (T) + 1 \in (y + 1 + 1 \dots N) \to y + 1 + 1 \leq 2^{nd} (T) + 1$
364	362 363	nsyl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \neg 2^{nd} (T) + 1 \in (y + 1 + 1 \dots N)$
365		disjsn	$⊢ (y + 1 + 1 \dots N) \cap \{2^{nd} (T) + 1\} = \emptyset \leftrightarrow \neg 2^{nd} (T) + 1 \in (y + 1 + 1 \dots N)$
366	364 365	sylibr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (y + 1 + 1 \dots N) \cap \{2^{nd} (T) + 1\} = \emptyset$
367	358 366	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ((y + 1 + 1 \dots N) \cap \{2^{nd} (T)\}) \cup ((y + 1 + 1 \dots N) \cap \{2^{nd} (T) + 1\}) = \emptyset \cup \emptyset$
368	140	ineq2i	$⊢ (y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = (y + 1 + 1 \dots N) \cap (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})$
369		indi	$⊢ (y + 1 + 1 \dots N) \cap (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}) = ((y + 1 + 1 \dots N) \cap \{2^{nd} (T)\}) \cup ((y + 1 + 1 \dots N) \cap \{2^{nd} (T) + 1\})$
370	368 369	eqtr2i	$⊢ ((y + 1 + 1 \dots N) \cap \{2^{nd} (T)\}) \cup ((y + 1 + 1 \dots N) \cap \{2^{nd} (T) + 1\}) = (y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\}$
371	367 370 144	3eqtr3g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset$
372	340 371	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (y + 1 + 1 \dots N) = \emptyset$
373		fnimadisj	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\} \land \{2^{nd} (T), 2^{nd} (T) + 1\} \cap (y + 1 + 1 \dots N) = \emptyset) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 + 1 \dots N)] = \emptyset$
374	339 372 373	syl2anc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 + 1 \dots N)] = \emptyset$
375	342 226	eleqtrdi	$⊢ y \in (0 \dots N - 1) \to y + 1 + 1 \in ℤ_{\geq 1}$
376		fzss1	$⊢ y + 1 + 1 \in ℤ_{\geq 1} \to (y + 1 + 1 \dots N) \subseteq (1 \dots N)$
377		reldisj	$⊢ (y + 1 + 1 \dots N) \subseteq (1 \dots N) \to ((y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (y + 1 + 1 \dots N) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
378	375 376 377	3syl	$⊢ y \in (0 \dots N - 1) \to ((y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (y + 1 + 1 \dots N) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
379	378	ad2antlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ((y + 1 + 1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \emptyset \leftrightarrow (y + 1 + 1 \dots N) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
380	371 379	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (y + 1 + 1 \dots N) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
381		resiima	$⊢ (y + 1 + 1 \dots N) \subseteq (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 + 1 \dots N)] = (y + 1 + 1 \dots N)$
382	380 381	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 + 1 \dots N)] = (y + 1 + 1 \dots N)$
383	374 382	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 + 1 \dots N)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 + 1 \dots N)] = \emptyset \cup (y + 1 + 1 \dots N)$
384		imaundir	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 + 1 \dots N)] = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} [(y + 1 + 1 \dots N)] \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) [(y + 1 + 1 \dots N)]$
385		uncom	$⊢ \emptyset \cup (y + 1 + 1 \dots N) = (y + 1 + 1 \dots N) \cup \emptyset$
386		un0	$⊢ (y + 1 + 1 \dots N) \cup \emptyset = (y + 1 + 1 \dots N)$
387	385 386	eqtr2i	$⊢ (y + 1 + 1 \dots N) = \emptyset \cup (y + 1 + 1 \dots N)$
388	383 384 387	3eqtr4g	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 + 1 \dots N)] = (y + 1 + 1 \dots N)$
389	388	imaeq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to 2^{nd} (1^{st} (T)) [(\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) [(y + 1 + 1 \dots N)]] = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
390	338 389	syl5eq	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
391	390	xpeq1d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}$
392	337 391	uneq12d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (T) \leq y) \to ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
393	277 392	syldan	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
394	393	oveq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
395		iffalse	$⊢ \neg y < 2^{nd} (T) \to if (y < 2^{nd} (T), y, y + 1) = y + 1$
396	395	csbeq1d	$⊢ \neg y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))$
397		ovex	$⊢ y + 1 \in V$
398		oveq2	$⊢ j = y + 1 \to (1 \dots j) = (1 \dots y + 1)$
399	398	imaeq2d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)]$
400	399	xpeq1d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}$
401		oveq1	$⊢ j = y + 1 \to j + 1 = y + 1 + 1$
402	401	oveq1d	$⊢ j = y + 1 \to (j + 1 \dots N) = (y + 1 + 1 \dots N)$
403	402	imaeq2d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)]$
404	403	xpeq1d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}$
405	400 404	uneq12d	$⊢ j = y + 1 \to ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\})$
406	405	oveq2d	$⊢ j = y + 1 \to 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}))$
407	397 406	csbie	$⊢ ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}))$
408	396 407	eqtrdi	$⊢ \neg y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}))$
409	408	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(y + 1 + 1 \dots N)] \times \{0\}))$
410	395	csbeq1d	$⊢ \neg y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
411	398	imaeq2d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
412	411	xpeq1d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}$
413	402	imaeq2d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
414	413	xpeq1d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}$
415	412 414	uneq12d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
416	415	oveq2d	$⊢ j = y + 1 \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
417	397 416	csbie	$⊢ ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
418	410 417	eqtrdi	$⊢ \neg y < 2^{nd} (T) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
419	418	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
420	394 409 419	3eqtr4d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
421	274 420	pm2.61dan	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
422	421	mpteq2dva	$⊢ φ \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
423	109 422	eqtr4d	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))))$
424		opex	$⊢ ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \in V$
425	424 24	op1std	$⊢ t = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \to 1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩$
426	424 24	op2ndd	$⊢ t = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \to 2^{nd} (t) = 2^{nd} (T)$
427		breq2	$⊢ 2^{nd} (t) = 2^{nd} (T) \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
428	427	ifbid	$⊢ 2^{nd} (t) = 2^{nd} (T) \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
429	428	csbeq1d	$⊢ 2^{nd} (t) = 2^{nd} (T) \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))$
430		fvex	$⊢ 1^{st} (1^{st} (T)) \in V$
431	430 80	op1std	$⊢ 1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
432	430 80	op2ndd	$⊢ 1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
433		id	$⊢ 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T)) \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
434		imaeq1	$⊢ 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)]$
435	434	xpeq1d	$⊢ 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}$
436		imaeq1	$⊢ 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)]$
437	436	xpeq1d	$⊢ 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}$
438	435 437	uneq12d	$⊢ 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})$
439	433 438	oveqan12d	$⊢ (1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))$
440	431 432 439	syl2anc	$⊢ 1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))$
441	440	csbeq2dv	$⊢ 1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))$
442	429 441	sylan9eqr	$⊢ (1^{st} (t) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \land 2^{nd} (t) = 2^{nd} (T)) \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))$
443	425 426 442	syl2anc	$⊢ t = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))$
444	443	mpteq2dv	$⊢ t = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\}))))$
445	444	eqeq2d	$⊢ t = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))))$
446	445 2	elrab2	$⊢ ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in S \leftrightarrow (⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} (((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) [(j + 1 \dots N)] \times \{0\})))))$
447	90 423 446	sylanbrc	$⊢ φ \to ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in S$

Metamath Proof Explorer

Theorem poimirlem15

Proof