poimirlem4

Description: Lemma for poimir connecting the admissible faces on the back face of the ( M + 1 ) -cube to admissible simplices in the M -cube. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem4.1	$⊢ φ \to K \in ℕ$
	poimirlem4.2	$⊢ φ \to M \in ℕ_{0}$
	poimirlem4.3	$⊢ φ \to M < N$
Assertion	poimirlem4	$⊢ φ \to \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \approx \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\}$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem4.1	$⊢ φ \to K \in ℕ$
3		poimirlem4.2	$⊢ φ \to M \in ℕ_{0}$
4		poimirlem4.3	$⊢ φ \to M < N$
5	1	adantr	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to N \in ℕ$
6	2	adantr	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to K \in ℕ$
7	3	adantr	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to M \in ℕ_{0}$
8	4	adantr	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to M < N$
9		xp1st	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 1^{st} (t) \in ({(0 ..^K)}^{(1 \dots M)})$
10		elmapi	$⊢ 1^{st} (t) \in ({(0 ..^K)}^{(1 \dots M)}) \to 1^{st} (t) : (1 \dots M) ⟶ (0 ..^K)$
11	9 10	syl	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 1^{st} (t) : (1 \dots M) ⟶ (0 ..^K)$
12	11	adantl	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 1^{st} (t) : (1 \dots M) ⟶ (0 ..^K)$
13		xp2nd	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 2^{nd} (t) \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}$
14		fvex	$⊢ 2^{nd} (t) \in V$
15		f1oeq1	$⊢ f = 2^{nd} (t) \to (f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \leftrightarrow 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M))$
16	14 15	elab	$⊢ 2^{nd} (t) \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \leftrightarrow 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
17	13 16	sylib	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
18	17	adantl	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
19	5 6 7 8 12 18	poimirlem3	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to (⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1)))$
20		fvex	$⊢ 1^{st} (t) \in V$
21		snex	$⊢ \{⟨M + 1, 0⟩\} \in V$
22	20 21	unex	$⊢ 1^{st} (t) \cup \{⟨M + 1, 0⟩\} \in V$
23		snex	$⊢ \{⟨M + 1, M + 1⟩\} \in V$
24	14 23	unex	$⊢ 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} \in V$
25	22 24	op1std	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 1^{st} (s) = 1^{st} (t) \cup \{⟨M + 1, 0⟩\}$
26	22 24	op2ndd	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) = 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}$
27	26	imaeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) [(1 \dots j)] = (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)]$
28	27	xpeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}$
29	26	imaeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) [(j + 1 \dots M + 1)] = (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
30	29	xpeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\} = (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}$
31	28 30	uneq12d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})$
32	25 31	oveq12d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\})) = (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))$
33	32	uneq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = ((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})$
34	33	csbeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B$
35	34	eqeq2d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
36	35	rexbidv	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (\exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
37	36	ralbidv	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
38	25	fveq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 1^{st} (s) (M + 1) = (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) (M + 1)$
39	38	eqeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (1^{st} (s) (M + 1) = 0 \leftrightarrow (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0)$
40	26	fveq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to 2^{nd} (s) (M + 1) = (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) (M + 1)$
41	40	eqeq1d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (2^{nd} (s) (M + 1) = M + 1 \leftrightarrow (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1)$
42	37 39 41	3anbi123d	$⊢ s = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1) \leftrightarrow (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1))$
43	42	elrab	$⊢ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \leftrightarrow (⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((1^{st} (t) \cup \{⟨M + 1, 0⟩\}) +_{f} (((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1))$
44	19 43	syl6ibr	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\})$
45	44	ralrimiva	$⊢ φ \to \forall t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\})$
46		fveq2	$⊢ s = t \to 1^{st} (s) = 1^{st} (t)$
47		fveq2	$⊢ s = t \to 2^{nd} (s) = 2^{nd} (t)$
48	47	imaeq1d	$⊢ s = t \to 2^{nd} (s) [(1 \dots j)] = 2^{nd} (t) [(1 \dots j)]$
49	48	xpeq1d	$⊢ s = t \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = 2^{nd} (t) [(1 \dots j)] \times \{1\}$
50	47	imaeq1d	$⊢ s = t \to 2^{nd} (s) [(j + 1 \dots M)] = 2^{nd} (t) [(j + 1 \dots M)]$
51	50	xpeq1d	$⊢ s = t \to 2^{nd} (s) [(j + 1 \dots M)] \times \{0\} = 2^{nd} (t) [(j + 1 \dots M)] \times \{0\}$
52	49 51	uneq12d	$⊢ s = t \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}) = (2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\})$
53	46 52	oveq12d	$⊢ s = t \to 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\})) = 1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))$
54	53	uneq1d	$⊢ s = t \to (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = (1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})$
55	54	csbeq1d	$⊢ s = t \to ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B$
56	55	eqeq2d	$⊢ s = t \to (i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
57	56	rexbidv	$⊢ s = t \to (\exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
58	57	ralbidv	$⊢ s = t \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
59	58	ralrab	$⊢ \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \leftrightarrow \forall t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\})$
60	45 59	sylibr	$⊢ φ \to \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\}$
61		xp1st	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 1^{st} (k) \in ({(0 ..^K)}^{(1 \dots M + 1)})$
62		elmapi	$⊢ 1^{st} (k) \in ({(0 ..^K)}^{(1 \dots M + 1)}) \to 1^{st} (k) : (1 \dots M + 1) ⟶ (0 ..^K)$
63	61 62	syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 1^{st} (k) : (1 \dots M + 1) ⟶ (0 ..^K)$
64		fzssp1	$⊢ (1 \dots M) \subseteq (1 \dots M + 1)$
65		fssres	$⊢ (1^{st} (k) : (1 \dots M + 1) ⟶ (0 ..^K) \land (1 \dots M) \subseteq (1 \dots M + 1)) \to ({1^{st} (k) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ (0 ..^K)$
66	63 64 65	sylancl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to ({1^{st} (k) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ (0 ..^K)$
67		ovex	$⊢ (0 ..^K) \in V$
68		ovex	$⊢ (1 \dots M) \in V$
69	67 68	elmap	$⊢ {1^{st} (k) ↾}_{(1 \dots M)} \in ({(0 ..^K)}^{(1 \dots M)}) \leftrightarrow ({1^{st} (k) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ (0 ..^K)$
70	66 69	sylibr	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to {1^{st} (k) ↾}_{(1 \dots M)} \in ({(0 ..^K)}^{(1 \dots M)})$
71	70	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to {1^{st} (k) ↾}_{(1 \dots M)} \in ({(0 ..^K)}^{(1 \dots M)})$
72		xp2nd	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}$
73		fvex	$⊢ 2^{nd} (k) \in V$
74		f1oeq1	$⊢ f = 2^{nd} (k) \to (f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \leftrightarrow 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1))$
75	73 74	elab	$⊢ 2^{nd} (k) \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\} \leftrightarrow 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)$
76	72 75	sylib	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)$
77		f1of1	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \to 2^{nd} (k) : (1 \dots M + 1) \underset{1-1}{⟶} (1 \dots M + 1)$
78	76 77	syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) : (1 \dots M + 1) \underset{1-1}{⟶} (1 \dots M + 1)$
79		f1ores	$⊢ (2^{nd} (k) : (1 \dots M + 1) \underset{1-1}{⟶} (1 \dots M + 1) \land (1 \dots M) \subseteq (1 \dots M + 1)) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} 2^{nd} (k) [(1 \dots M)]$
80	78 64 79	sylancl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} 2^{nd} (k) [(1 \dots M)]$
81	80	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} 2^{nd} (k) [(1 \dots M)]$
82		dff1o3	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \leftrightarrow (2^{nd} (k) : (1 \dots M + 1) \underset{onto}{⟶} (1 \dots M + 1) \land Fun {2^{nd} (k)}^{-1})$
83	82	simprbi	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \to Fun {2^{nd} (k)}^{-1}$
84		imadif	$⊢ Fun {2^{nd} (k)}^{-1} \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}]$
85	76 83 84	3syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}]$
86	85	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}]$
87		f1ofo	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \to 2^{nd} (k) : (1 \dots M + 1) \underset{onto}{⟶} (1 \dots M + 1)$
88		foima	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{onto}{⟶} (1 \dots M + 1) \to 2^{nd} (k) [(1 \dots M + 1)] = (1 \dots M + 1)$
89	76 87 88	3syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) [(1 \dots M + 1)] = (1 \dots M + 1)$
90	89	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M + 1)] = (1 \dots M + 1)$
91		f1ofn	$⊢ 2^{nd} (k) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \to 2^{nd} (k) Fn (1 \dots M + 1)$
92	76 91	syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) Fn (1 \dots M + 1)$
93		nn0p1nn	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ$
94	3 93	syl	$⊢ φ \to M + 1 \in ℕ$
95		elfz1end	$⊢ M + 1 \in ℕ \leftrightarrow M + 1 \in (1 \dots M + 1)$
96	94 95	sylib	$⊢ φ \to M + 1 \in (1 \dots M + 1)$
97		fnsnfv	$⊢ (2^{nd} (k) Fn (1 \dots M + 1) \land M + 1 \in (1 \dots M + 1)) \to \{2^{nd} (k) (M + 1)\} = 2^{nd} (k) [\{M + 1\}]$
98	92 96 97	syl2anr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to \{2^{nd} (k) (M + 1)\} = 2^{nd} (k) [\{M + 1\}]$
99		sneq	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to \{2^{nd} (k) (M + 1)\} = \{M + 1\}$
100	98 99	sylan9req	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [\{M + 1\}] = \{M + 1\}$
101	90 100	difeq12d	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}] = (1 \dots M + 1) ∖ \{M + 1\}$
102	86 101	eqtrd	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = (1 \dots M + 1) ∖ \{M + 1\}$
103		1z	$⊢ 1 \in ℤ$
104		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
105		1m1e0	$⊢ 1 - 1 = 0$
106	105	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
107	104 106	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
108	3 107	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (1 - 1)}$
109		fzsuc2	$⊢ (1 \in ℤ \land M \in ℤ_{\geq (1 - 1)}) \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
110	103 108 109	sylancr	$⊢ φ \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
111	110	difeq1d	$⊢ φ \to (1 \dots M + 1) ∖ \{M + 1\} = ((1 \dots M) \cup \{M + 1\}) ∖ \{M + 1\}$
112		difun2	$⊢ ((1 \dots M) \cup \{M + 1\}) ∖ \{M + 1\} = (1 \dots M) ∖ \{M + 1\}$
113	111 112	eqtrdi	$⊢ φ \to (1 \dots M + 1) ∖ \{M + 1\} = (1 \dots M) ∖ \{M + 1\}$
114	3	nn0red	$⊢ φ \to M \in ℝ$
115		ltp1	$⊢ M \in ℝ \to M < M + 1$
116		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
117		ltnle	$⊢ (M \in ℝ \land M + 1 \in ℝ) \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
118	116 117	mpdan	$⊢ M \in ℝ \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
119	115 118	mpbid	$⊢ M \in ℝ \to \neg M + 1 \leq M$
120	114 119	syl	$⊢ φ \to \neg M + 1 \leq M$
121		elfzle2	$⊢ M + 1 \in (1 \dots M) \to M + 1 \leq M$
122	120 121	nsyl	$⊢ φ \to \neg M + 1 \in (1 \dots M)$
123		difsn	$⊢ \neg M + 1 \in (1 \dots M) \to (1 \dots M) ∖ \{M + 1\} = (1 \dots M)$
124	122 123	syl	$⊢ φ \to (1 \dots M) ∖ \{M + 1\} = (1 \dots M)$
125	113 124	eqtrd	$⊢ φ \to (1 \dots M + 1) ∖ \{M + 1\} = (1 \dots M)$
126	125	imaeq2d	$⊢ φ \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M)]$
127	126	ad2antrr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M)]$
128	125	ad2antrr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to (1 \dots M + 1) ∖ \{M + 1\} = (1 \dots M)$
129	102 127 128	3eqtr3d	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots M)] = (1 \dots M)$
130		f1oeq3	$⊢ 2^{nd} (k) [(1 \dots M)] = (1 \dots M) \to (({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} 2^{nd} (k) [(1 \dots M)] \leftrightarrow ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M))$
131	129 130	syl	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to (({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} 2^{nd} (k) [(1 \dots M)] \leftrightarrow ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M))$
132	81 131	mpbid	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
133	73	resex	$⊢ {2^{nd} (k) ↾}_{(1 \dots M)} \in V$
134		f1oeq1	$⊢ f = {2^{nd} (k) ↾}_{(1 \dots M)} \to (f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \leftrightarrow ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M))$
135	133 134	elab	$⊢ {2^{nd} (k) ↾}_{(1 \dots M)} \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \leftrightarrow ({2^{nd} (k) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
136	132 135	sylibr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to {2^{nd} (k) ↾}_{(1 \dots M)} \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}$
137		opelxpi	$⊢ ({1^{st} (k) ↾}_{(1 \dots M)} \in ({(0 ..^K)}^{(1 \dots M)}) \land {2^{nd} (k) ↾}_{(1 \dots M)} \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})$
138	71 136 137	syl2anc	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})$
139	138	3ad2antr3	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})$
140		3anass	$⊢ (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \leftrightarrow (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1))$
141		ancom	$⊢ (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \leftrightarrow ((1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \land \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
142	140 141	bitri	$⊢ (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \leftrightarrow ((1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \land \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
143	94	nnzd	$⊢ φ \to M + 1 \in ℤ$
144		uzid	$⊢ M + 1 \in ℤ \to M + 1 \in ℤ_{\geq (M + 1)}$
145		peano2uz	$⊢ M + 1 \in ℤ_{\geq (M + 1)} \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
146	143 144 145	3syl	$⊢ φ \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
147	3	nn0zd	$⊢ φ \to M \in ℤ$
148	1	nnzd	$⊢ φ \to N \in ℤ$
149		zltp1le	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow M + 1 \leq N)$
150		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
151		eluz	$⊢ (M + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
152	150 151	sylan	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
153	149 152	bitr4d	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
154	147 148 153	syl2anc	$⊢ φ \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
155	4 154	mpbid	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
156		fzsplit2	$⊢ (M + 1 + 1 \in ℤ_{\geq (M + 1)} \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 \dots N) = (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
157	146 155 156	syl2anc	$⊢ φ \to (M + 1 \dots N) = (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
158		fzsn	$⊢ M + 1 \in ℤ \to (M + 1 \dots M + 1) = \{M + 1\}$
159	143 158	syl	$⊢ φ \to (M + 1 \dots M + 1) = \{M + 1\}$
160	159	uneq1d	$⊢ φ \to (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
161	157 160	eqtrd	$⊢ φ \to (M + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
162	161	xpeq1d	$⊢ φ \to (M + 1 \dots N) \times \{0\} = (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\}$
163	162	uneq2d	$⊢ φ \to (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\})$
164		xpundir	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
165		ovex	$⊢ M + 1 \in V$
166		c0ex	$⊢ 0 \in V$
167	165 166	xpsn	$⊢ \{M + 1\} \times \{0\} = \{⟨M + 1, 0⟩\}$
168	167	uneq1i	$⊢ (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
169	164 168	eqtri	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
170	169	uneq2i	$⊢ (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\}) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup (\{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\}))$
171		unass	$⊢ ((n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup (\{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\}))$
172	170 171	eqtr4i	$⊢ (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\}) = ((n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
173	163 172	eqtrdi	$⊢ φ \to (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\}) = ((n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
174	173	ad3antrrr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\}) = ((n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
175	165	a1i	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to M + 1 \in V$
176	166	a1i	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to 0 \in V$
177	110	eqcomd	$⊢ φ \to (1 \dots M) \cup \{M + 1\} = (1 \dots M + 1)$
178	177	ad3antrrr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (1 \dots M) \cup \{M + 1\} = (1 \dots M + 1)$
179		fveq2	$⊢ n = M + 1 \to 1^{st} (k) (n) = 1^{st} (k) (M + 1)$
180		fveq2	$⊢ n = M + 1 \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1)$
181	179 180	oveq12d	$⊢ n = M + 1 \to 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = 1^{st} (k) (M + 1) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1)$
182		simplrl	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to 1^{st} (k) (M + 1) = 0$
183		imain	$⊢ Fun {2^{nd} (k)}^{-1} \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)]$
184	76 83 183	3syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)]$
185	184	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)]$
186		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
187	186	nn0red	$⊢ j \in (0 \dots M) \to j \in ℝ$
188	187	ltp1d	$⊢ j \in (0 \dots M) \to j < j + 1$
189		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
190	188 189	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
191	190	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = 2^{nd} (k) [\emptyset]$
192		ima0	$⊢ 2^{nd} (k) [\emptyset] = \emptyset$
193	191 192	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = \emptyset$
194	185 193	sylan9req	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)] = \emptyset$
195		simplr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) (M + 1) = M + 1$
196	92	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) Fn (1 \dots M + 1)$
197		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
198		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
199	197 198	eleqtrdi	$⊢ j \in ℕ_{0} \to j + 1 \in ℤ_{\geq 1}$
200		fzss1	$⊢ j + 1 \in ℤ_{\geq 1} \to (j + 1 \dots M + 1) \subseteq (1 \dots M + 1)$
201	186 199 200	3syl	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \subseteq (1 \dots M + 1)$
202		elfzuz3	$⊢ j \in (0 \dots M) \to M \in ℤ_{\geq j}$
203		eluzp1p1	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq (j + 1)}$
204		eluzfz2	$⊢ M + 1 \in ℤ_{\geq (j + 1)} \to M + 1 \in (j + 1 \dots M + 1)$
205	202 203 204	3syl	$⊢ j \in (0 \dots M) \to M + 1 \in (j + 1 \dots M + 1)$
206	201 205	jca	$⊢ j \in (0 \dots M) \to ((j + 1 \dots M + 1) \subseteq (1 \dots M + 1) \land M + 1 \in (j + 1 \dots M + 1))$
207		fnfvima	$⊢ (2^{nd} (k) Fn (1 \dots M + 1) \land (j + 1 \dots M + 1) \subseteq (1 \dots M + 1) \land M + 1 \in (j + 1 \dots M + 1)) \to 2^{nd} (k) (M + 1) \in 2^{nd} (k) [(j + 1 \dots M + 1)]$
208	207	3expb	$⊢ (2^{nd} (k) Fn (1 \dots M + 1) \land ((j + 1 \dots M + 1) \subseteq (1 \dots M + 1) \land M + 1 \in (j + 1 \dots M + 1))) \to 2^{nd} (k) (M + 1) \in 2^{nd} (k) [(j + 1 \dots M + 1)]$
209	196 206 208	syl2an	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) (M + 1) \in 2^{nd} (k) [(j + 1 \dots M + 1)]$
210	195 209	eqeltrrd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to M + 1 \in 2^{nd} (k) [(j + 1 \dots M + 1)]$
211		1ex	$⊢ 1 \in V$
212		fnconstg	$⊢ 1 \in V \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)]$
213	211 212	ax-mp	$⊢ (2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)]$
214		fnconstg	$⊢ 0 \in V \to (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)]$
215	166 214	ax-mp	$⊢ (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)]$
216		fvun2	$⊢ ((2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)] \land (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)] \land (2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)] = \emptyset \land M + 1 \in 2^{nd} (k) [(j + 1 \dots M + 1)])) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
217	213 215 216	mp3an12	$⊢ (2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)] = \emptyset \land M + 1 \in 2^{nd} (k) [(j + 1 \dots M + 1)]) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
218	194 210 217	syl2anc	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
219	166	fvconst2	$⊢ M + 1 \in 2^{nd} (k) [(j + 1 \dots M + 1)] \to (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1) = 0$
220	210 219	syl	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1) = 0$
221	218 220	eqtrd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = 0$
222	221	adantlrl	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = 0$
223	182 222	oveq12d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to 1^{st} (k) (M + 1) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = 0 + 0$
224		00id	$⊢ 0 + 0 = 0$
225	223 224	eqtrdi	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to 1^{st} (k) (M + 1) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = 0$
226	181 225	sylan9eqr	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \land n = M + 1) \to 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = 0$
227	175 176 178 226	fmptapd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\} = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n))$
228	227	uneq1d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to ((n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 + 1 \dots N) \times \{0\})$
229	174 228	eqtrd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\}) = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 + 1 \dots N) \times \{0\})$
230		elmapfn	$⊢ 1^{st} (k) \in ({(0 ..^K)}^{(1 \dots M + 1)}) \to 1^{st} (k) Fn (1 \dots M + 1)$
231	61 230	syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 1^{st} (k) Fn (1 \dots M + 1)$
232		fnssres	$⊢ (1^{st} (k) Fn (1 \dots M + 1) \land (1 \dots M) \subseteq (1 \dots M + 1)) \to ({1^{st} (k) ↾}_{(1 \dots M)}) Fn (1 \dots M)$
233	231 64 232	sylancl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to ({1^{st} (k) ↾}_{(1 \dots M)}) Fn (1 \dots M)$
234	233	ad3antlr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ({1^{st} (k) ↾}_{(1 \dots M)}) Fn (1 \dots M)$
235		simplr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})$
236		fnconstg	$⊢ 0 \in V \to (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)]$
237	166 236	ax-mp	$⊢ (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)]$
238	213 237	pm3.2i	$⊢ ((2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)] \land (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)])$
239		imain	$⊢ Fun {2^{nd} (k)}^{-1} \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M)]$
240	76 83 239	3syl	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M)]$
241		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
242	188 241	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
243	242	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = 2^{nd} (k) [\emptyset]$
244	243 192	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = \emptyset$
245	240 244	sylan9req	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M)] = \emptyset$
246		fnun	$⊢ (((2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)] \land (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)]) \land 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M)] = \emptyset) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)])$
247	238 245 246	sylancr	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)])$
248	235 247	sylan	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)])$
249	101	adantr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}] = (1 \dots M + 1) ∖ \{M + 1\}$
250	85	ad3antlr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}]$
251	186 197	syl	$⊢ j \in (0 \dots M) \to j + 1 \in ℕ$
252	251 198	eleqtrdi	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ_{\geq 1}$
253		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land M \in ℤ_{\geq j}) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
254	252 202 253	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
255	128 254	sylan9eq	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M + 1) ∖ \{M + 1\} = (1 \dots j) \cup (j + 1 \dots M)$
256	255	imaeq2d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots M + 1) ∖ \{M + 1\}] = 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M)]$
257	250 256	eqtr3d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots M + 1)] ∖ 2^{nd} (k) [\{M + 1\}] = 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M)]$
258	125	ad3antrrr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M + 1) ∖ \{M + 1\} = (1 \dots M)$
259	249 257 258	3eqtr3rd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M) = 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M)]$
260		imaundi	$⊢ 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M)] = 2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)]$
261	259 260	eqtrdi	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M) = 2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)]$
262	261	fneq2d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \leftrightarrow ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M)]))$
263	248 262	mpbird	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M)$
264		fzss2	$⊢ M \in ℤ_{\geq j} \to (1 \dots j) \subseteq (1 \dots M)$
265		resima2	$⊢ (1 \dots j) \subseteq (1 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
266	202 264 265	3syl	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
267	266	xpeq1d	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\} = 2^{nd} (k) [(1 \dots j)] \times \{1\}$
268	186 199	syl	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ_{\geq 1}$
269		fzss1	$⊢ j + 1 \in ℤ_{\geq 1} \to (j + 1 \dots M) \subseteq (1 \dots M)$
270		resima2	$⊢ (j + 1 \dots M) \subseteq (1 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] = 2^{nd} (k) [(j + 1 \dots M)]$
271	268 269 270	3syl	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] = 2^{nd} (k) [(j + 1 \dots M)]$
272	271	xpeq1d	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\} = 2^{nd} (k) [(j + 1 \dots M)] \times \{0\}$
273	267 272	uneq12d	$⊢ j \in (0 \dots M) \to (({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}) = (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})$
274	273	adantl	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}) = (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})$
275	274	fneq1d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \leftrightarrow ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M))$
276	263 275	mpbird	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M)$
277		fzfid	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M) \in Fin$
278		inidm	$⊢ (1 \dots M) \cap (1 \dots M) = (1 \dots M)$
279		fvres	$⊢ n \in (1 \dots M) \to ({1^{st} (k) ↾}_{(1 \dots M)}) (n) = 1^{st} (k) (n)$
280	279	adantl	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to ({1^{st} (k) ↾}_{(1 \dots M)}) (n) = 1^{st} (k) (n)$
281		disjsn	$⊢ (1 \dots M) \cap \{M + 1\} = \emptyset \leftrightarrow \neg M + 1 \in (1 \dots M)$
282	122 281	sylibr	$⊢ φ \to (1 \dots M) \cap \{M + 1\} = \emptyset$
283	282	ad3antrrr	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (1 \dots M) \cap \{M + 1\} = \emptyset$
284	263 283	jca	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset)$
285		fnconstg	$⊢ 0 \in V \to (\{M + 1\} \times \{0\}) Fn \{M + 1\}$
286	166 285	ax-mp	$⊢ (\{M + 1\} \times \{0\}) Fn \{M + 1\}$
287		fvun1	$⊢ (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \land (\{M + 1\} \times \{0\}) Fn \{M + 1\} \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land n \in (1 \dots M))) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
288	286 287	mp3an2	$⊢ (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land n \in (1 \dots M))) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
289	288	anassrs	$⊢ ((((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \land n \in (1 \dots M)) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
290	284 289	sylan	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
291	251	nnzd	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ$
292	186	nn0cnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
293		pncan1	$⊢ j \in ℂ \to j + 1 - 1 = j$
294	292 293	syl	$⊢ j \in (0 \dots M) \to j + 1 - 1 = j$
295	294	fveq2d	$⊢ j \in (0 \dots M) \to ℤ_{\geq (j + 1 - 1)} = ℤ_{\geq j}$
296	202 295	eleqtrrd	$⊢ j \in (0 \dots M) \to M \in ℤ_{\geq (j + 1 - 1)}$
297		fzsuc2	$⊢ (j + 1 \in ℤ \land M \in ℤ_{\geq (j + 1 - 1)}) \to (j + 1 \dots M + 1) = (j + 1 \dots M) \cup \{M + 1\}$
298	291 296 297	syl2anc	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) = (j + 1 \dots M) \cup \{M + 1\}$
299	298	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(j + 1 \dots M + 1)] = 2^{nd} (k) [(j + 1 \dots M) \cup \{M + 1\}]$
300		imaundi	$⊢ 2^{nd} (k) [(j + 1 \dots M) \cup \{M + 1\}] = 2^{nd} (k) [(j + 1 \dots M)] \cup 2^{nd} (k) [\{M + 1\}]$
301	299 300	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(j + 1 \dots M + 1)] = 2^{nd} (k) [(j + 1 \dots M)] \cup 2^{nd} (k) [\{M + 1\}]$
302	301	xpeq1d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\} = (2^{nd} (k) [(j + 1 \dots M)] \cup 2^{nd} (k) [\{M + 1\}]) \times \{0\}$
303		xpundir	$⊢ (2^{nd} (k) [(j + 1 \dots M)] \cup 2^{nd} (k) [\{M + 1\}]) \times \{0\} = (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
304	302 303	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\} = (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
305	304	uneq2d	$⊢ j \in (0 \dots M) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\}))$
306		unass	$⊢ ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\}) = (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\}))$
307	305 306	eqtr4di	$⊢ j \in (0 \dots M) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
308	307	adantl	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land j \in (0 \dots M)) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
309	98	xpeq1d	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to \{2^{nd} (k) (M + 1)\} \times \{0\} = 2^{nd} (k) [\{M + 1\}] \times \{0\}$
310	309	uneq2d	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{2^{nd} (k) (M + 1)\} \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
311	310	adantr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{2^{nd} (k) (M + 1)\} \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (2^{nd} (k) [\{M + 1\}] \times \{0\})$
312	308 311	eqtr4d	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land j \in (0 \dots M)) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{2^{nd} (k) (M + 1)\} \times \{0\})$
313	99	xpeq1d	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to \{2^{nd} (k) (M + 1)\} \times \{0\} = \{M + 1\} \times \{0\}$
314	313	uneq2d	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{2^{nd} (k) (M + 1)\} \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})$
315	312 314	sylan9eq	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land j \in (0 \dots M)) \land 2^{nd} (k) (M + 1) = M + 1) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})$
316	315	an32s	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})$
317	316	fveq1d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n)$
318	317	adantr	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) \cup (\{M + 1\} \times \{0\})) (n)$
319	273	fveq1d	$⊢ j \in (0 \dots M) \to ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
320	319	ad2antlr	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M)] \times \{0\})) (n)$
321	290 318 320	3eqtr4rd	$⊢ ((((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)$
322	234 276 277 277 278 280 321	offval	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to ({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n))$
323	322	uneq1d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \land j \in (0 \dots M)) \to (({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\})$
324	323	adantlrl	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 \dots N) \times \{0\})$
325		simplr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})$
326	231	adantr	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to 1^{st} (k) Fn (1 \dots M + 1)$
327	213 215	pm3.2i	$⊢ ((2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)] \land (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)])$
328	184 193	sylan9req	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)] = \emptyset$
329		fnun	$⊢ (((2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)] \land (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)]) \land 2^{nd} (k) [(1 \dots j)] \cap 2^{nd} (k) [(j + 1 \dots M + 1)] = \emptyset) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)])$
330	327 328 329	sylancr	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)])$
331		peano2uz	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq j}$
332	202 331	syl	$⊢ j \in (0 \dots M) \to M + 1 \in ℤ_{\geq j}$
333		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land M + 1 \in ℤ_{\geq j}) \to (1 \dots M + 1) = (1 \dots j) \cup (j + 1 \dots M + 1)$
334	268 332 333	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M + 1) = (1 \dots j) \cup (j + 1 \dots M + 1)$
335	334	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots M + 1)] = 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M + 1)]$
336		imaundi	$⊢ 2^{nd} (k) [(1 \dots j) \cup (j + 1 \dots M + 1)] = 2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)]$
337	335 336	eqtr2di	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)] = 2^{nd} (k) [(1 \dots M + 1)]$
338	337 89	sylan9eqr	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to 2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)] = (1 \dots M + 1)$
339	338	fneq2d	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to (((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) Fn (2^{nd} (k) [(1 \dots j)] \cup 2^{nd} (k) [(j + 1 \dots M + 1)]) \leftrightarrow ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) Fn (1 \dots M + 1))$
340	330 339	mpbid	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) Fn (1 \dots M + 1)$
341		fzfid	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to (1 \dots M + 1) \in Fin$
342		inidm	$⊢ (1 \dots M + 1) \cap (1 \dots M + 1) = (1 \dots M + 1)$
343		eqidd	$⊢ ((k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \land n \in (1 \dots M + 1)) \to 1^{st} (k) (n) = 1^{st} (k) (n)$
344		eqidd	$⊢ ((k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \land n \in (1 \dots M + 1)) \to ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n) = ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)$
345	326 340 341 341 342 343 344	offval	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to 1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n))$
346	345	uneq1d	$⊢ (k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \land j \in (0 \dots M)) \to (1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 + 1 \dots N) \times \{0\})$
347	325 346	sylan	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (n \in (1 \dots M + 1) ⟼ 1^{st} (k) (n) + ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup ((M + 1 + 1 \dots N) \times \{0\})$
348	229 324 347	3eqtr4rd	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})$
349	348	csbeq1d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B$
350	349	eqeq2d	$⊢ (((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \land j \in (0 \dots M)) \to (i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
351	350	rexbidva	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to (\exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
352	351	ralbidv	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
353	352	biimpd	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \to \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
354	353	impr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land ((1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \land \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)) \to \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B$
355	142 354	sylan2b	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B$
356		1st2nd2	$⊢ k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \to k = ⟨1^{st} (k), 2^{nd} (k)⟩$
357	356	ad2antlr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to k = ⟨1^{st} (k), 2^{nd} (k)⟩$
358		fnsnsplit	$⊢ (1^{st} (k) Fn (1 \dots M + 1) \land M + 1 \in (1 \dots M + 1)) \to 1^{st} (k) = ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 1^{st} (k) (M + 1)⟩\}$
359	231 96 358	syl2anr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to 1^{st} (k) = ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 1^{st} (k) (M + 1)⟩\}$
360	359	adantr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 1^{st} (k) (M + 1) = 0) \to 1^{st} (k) = ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 1^{st} (k) (M + 1)⟩\}$
361	125	reseq2d	$⊢ φ \to {1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {1^{st} (k) ↾}_{(1 \dots M)}$
362	361	adantr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to {1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {1^{st} (k) ↾}_{(1 \dots M)}$
363		opeq2	$⊢ 1^{st} (k) (M + 1) = 0 \to ⟨M + 1, 1^{st} (k) (M + 1)⟩ = ⟨M + 1, 0⟩$
364	363	sneqd	$⊢ 1^{st} (k) (M + 1) = 0 \to \{⟨M + 1, 1^{st} (k) (M + 1)⟩\} = \{⟨M + 1, 0⟩\}$
365		uneq12	$⊢ ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {1^{st} (k) ↾}_{(1 \dots M)} \land \{⟨M + 1, 1^{st} (k) (M + 1)⟩\} = \{⟨M + 1, 0⟩\}) \to ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 1^{st} (k) (M + 1)⟩\} = ({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}$
366	362 364 365	syl2an	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 1^{st} (k) (M + 1) = 0) \to ({1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 1^{st} (k) (M + 1)⟩\} = ({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}$
367	360 366	eqtrd	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 1^{st} (k) (M + 1) = 0) \to 1^{st} (k) = ({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}$
368	367	adantrr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to 1^{st} (k) = ({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}$
369		fnsnsplit	$⊢ (2^{nd} (k) Fn (1 \dots M + 1) \land M + 1 \in (1 \dots M + 1)) \to 2^{nd} (k) = ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\}$
370	92 96 369	syl2anr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to 2^{nd} (k) = ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\}$
371	370	adantr	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) = ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\}$
372	125	reseq2d	$⊢ φ \to {2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {2^{nd} (k) ↾}_{(1 \dots M)}$
373	372	adantr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to {2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {2^{nd} (k) ↾}_{(1 \dots M)}$
374		opeq2	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to ⟨M + 1, 2^{nd} (k) (M + 1)⟩ = ⟨M + 1, M + 1⟩$
375	374	sneqd	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\} = \{⟨M + 1, M + 1⟩\}$
376		uneq12	$⊢ ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {2^{nd} (k) ↾}_{(1 \dots M)} \land \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\} = \{⟨M + 1, M + 1⟩\}) \to ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\} = ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}$
377	373 375 376	syl2an	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to ({2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})}) \cup \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\} = ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}$
378	371 377	eqtrd	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land 2^{nd} (k) (M + 1) = M + 1) \to 2^{nd} (k) = ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}$
379	378	adantrl	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to 2^{nd} (k) = ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}$
380	368 379	opeq12d	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to ⟨1^{st} (k), 2^{nd} (k)⟩ = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩$
381	357 380	eqtrd	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to k = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩$
382	381	3adantr1	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to k = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩$
383		fvex	$⊢ 1^{st} (k) \in V$
384	383	resex	$⊢ {1^{st} (k) ↾}_{(1 \dots M)} \in V$
385	384 133	op1std	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 1^{st} (t) = {1^{st} (k) ↾}_{(1 \dots M)}$
386	384 133	op2ndd	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) = {2^{nd} (k) ↾}_{(1 \dots M)}$
387	386	imaeq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) [(1 \dots j)] = ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)]$
388	387	xpeq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) [(1 \dots j)] \times \{1\} = ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}$
389	386	imaeq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) [(j + 1 \dots M)] = ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)]$
390	389	xpeq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) [(j + 1 \dots M)] \times \{0\} = ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}$
391	388 390	uneq12d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}) = (({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\})$
392	385 391	oveq12d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\})) = ({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))$
393	392	uneq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = (({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})$
394	393	csbeq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B$
395	394	eqeq2d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
396	395	rexbidv	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (\exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
397	396	ralbidv	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B)$
398	385	uneq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 1^{st} (t) \cup \{⟨M + 1, 0⟩\} = ({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}$
399	386	uneq1d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}$
400	398 399	opeq12d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩$
401	400	eqeq2d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to (k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow k = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩)$
402	397 401	anbi12d	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) \leftrightarrow (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩))$
403	402	rspcev	$⊢ (⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((({1^{st} (k) ↾}_{(1 \dots M)}) +_{f} ((({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] \times \{1\}) \cup (({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨({1^{st} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, 0⟩\}, ({2^{nd} (k) ↾}_{(1 \dots M)}) \cup \{⟨M + 1, M + 1⟩\}⟩)) \to \exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
404	139 355 382 403	syl12anc	$⊢ ((φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \land (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1)) \to \exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
405	404	ex	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \to \exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩))$
406		elrabi	$⊢ t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \to t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})$
407		elrabi	$⊢ n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \to n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})$
408	406 407	anim12i	$⊢ (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \land n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\}) \to (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))$
409		eqtr2	$⊢ (k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩$
410	22 24	opth	$⊢ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow (1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\} \land 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\})$
411		difeq1	$⊢ 1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\} \to (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\} = (1^{st} (n) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\}$
412		difun2	$⊢ (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (t) ∖ \{⟨M + 1, 0⟩\}$
413		difun2	$⊢ (1^{st} (n) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\}$
414	411 412 413	3eqtr3g	$⊢ 1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\} \to 1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\}$
415		difeq1	$⊢ 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\} \to (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\} = (2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\}$
416		difun2	$⊢ (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\}$
417		difun2	$⊢ (2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\}$
418	415 416 417	3eqtr3g	$⊢ 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\} \to 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\}$
419	414 418	anim12i	$⊢ (1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\} \land 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}) \to (1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \land 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\})$
420	410 419	sylbi	$⊢ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩ \to (1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \land 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\})$
421	409 420	syl	$⊢ (k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to (1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \land 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\})$
422		elmapfn	$⊢ 1^{st} (t) \in ({(0 ..^K)}^{(1 \dots M)}) \to 1^{st} (t) Fn (1 \dots M)$
423		fnop	$⊢ (1^{st} (t) Fn (1 \dots M) \land ⟨M + 1, 0⟩ \in 1^{st} (t)) \to M + 1 \in (1 \dots M)$
424	423	ex	$⊢ 1^{st} (t) Fn (1 \dots M) \to (⟨M + 1, 0⟩ \in 1^{st} (t) \to M + 1 \in (1 \dots M))$
425	9 422 424	3syl	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (⟨M + 1, 0⟩ \in 1^{st} (t) \to M + 1 \in (1 \dots M))$
426	425 122	nsyli	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (φ \to \neg ⟨M + 1, 0⟩ \in 1^{st} (t))$
427	426	impcom	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to \neg ⟨M + 1, 0⟩ \in 1^{st} (t)$
428		difsn	$⊢ \neg ⟨M + 1, 0⟩ \in 1^{st} (t) \to 1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (t)$
429	427 428	syl	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (t)$
430		xp1st	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 1^{st} (n) \in ({(0 ..^K)}^{(1 \dots M)})$
431		elmapfn	$⊢ 1^{st} (n) \in ({(0 ..^K)}^{(1 \dots M)}) \to 1^{st} (n) Fn (1 \dots M)$
432		fnop	$⊢ (1^{st} (n) Fn (1 \dots M) \land ⟨M + 1, 0⟩ \in 1^{st} (n)) \to M + 1 \in (1 \dots M)$
433	432	ex	$⊢ 1^{st} (n) Fn (1 \dots M) \to (⟨M + 1, 0⟩ \in 1^{st} (n) \to M + 1 \in (1 \dots M))$
434	430 431 433	3syl	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (⟨M + 1, 0⟩ \in 1^{st} (n) \to M + 1 \in (1 \dots M))$
435	434 122	nsyli	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (φ \to \neg ⟨M + 1, 0⟩ \in 1^{st} (n))$
436	435	impcom	$⊢ (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to \neg ⟨M + 1, 0⟩ \in 1^{st} (n)$
437		difsn	$⊢ \neg ⟨M + 1, 0⟩ \in 1^{st} (n) \to 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n)$
438	436 437	syl	$⊢ (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n)$
439	429 438	eqeqan12d	$⊢ ((φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \land (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to (1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \leftrightarrow 1^{st} (t) = 1^{st} (n))$
440	439	anandis	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to (1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \leftrightarrow 1^{st} (t) = 1^{st} (n))$
441		f1ofn	$⊢ 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to 2^{nd} (t) Fn (1 \dots M)$
442		fnop	$⊢ (2^{nd} (t) Fn (1 \dots M) \land ⟨M + 1, M + 1⟩ \in 2^{nd} (t)) \to M + 1 \in (1 \dots M)$
443	442	ex	$⊢ 2^{nd} (t) Fn (1 \dots M) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (t) \to M + 1 \in (1 \dots M))$
444	17 441 443	3syl	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (t) \to M + 1 \in (1 \dots M))$
445	444 122	nsyli	$⊢ t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (φ \to \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (t))$
446	445	impcom	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (t)$
447		difsn	$⊢ \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (t) \to 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (t)$
448	446 447	syl	$⊢ (φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (t)$
449		xp2nd	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 2^{nd} (n) \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}$
450		fvex	$⊢ 2^{nd} (n) \in V$
451		f1oeq1	$⊢ f = 2^{nd} (n) \to (f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \leftrightarrow 2^{nd} (n) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M))$
452	450 451	elab	$⊢ 2^{nd} (n) \in \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \leftrightarrow 2^{nd} (n) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
453	449 452	sylib	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to 2^{nd} (n) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
454		f1ofn	$⊢ 2^{nd} (n) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to 2^{nd} (n) Fn (1 \dots M)$
455		fnop	$⊢ (2^{nd} (n) Fn (1 \dots M) \land ⟨M + 1, M + 1⟩ \in 2^{nd} (n)) \to M + 1 \in (1 \dots M)$
456	455	ex	$⊢ 2^{nd} (n) Fn (1 \dots M) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (n) \to M + 1 \in (1 \dots M))$
457	453 454 456	3syl	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (n) \to M + 1 \in (1 \dots M))$
458	457 122	nsyli	$⊢ n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \to (φ \to \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (n))$
459	458	impcom	$⊢ (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (n)$
460		difsn	$⊢ \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (n) \to 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n)$
461	459 460	syl	$⊢ (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n)$
462	448 461	eqeqan12d	$⊢ ((φ \land t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \land (φ \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to (2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\} \leftrightarrow 2^{nd} (t) = 2^{nd} (n))$
463	462	anandis	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to (2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\} \leftrightarrow 2^{nd} (t) = 2^{nd} (n))$
464	440 463	anbi12d	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to ((1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \land 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\}) \leftrightarrow (1^{st} (t) = 1^{st} (n) \land 2^{nd} (t) = 2^{nd} (n)))$
465		xpopth	$⊢ (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\})) \to ((1^{st} (t) = 1^{st} (n) \land 2^{nd} (t) = 2^{nd} (n)) \leftrightarrow t = n)$
466	465	adantl	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to ((1^{st} (t) = 1^{st} (n) \land 2^{nd} (t) = 2^{nd} (n)) \leftrightarrow t = n)$
467	464 466	bitrd	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to ((1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} \land 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\}) \leftrightarrow t = n)$
468	421 467	syl5ib	$⊢ (φ \land (t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \land n \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}))) \to ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)$
469	408 468	sylan2	$⊢ (φ \land (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \land n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\})) \to ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)$
470	469	ralrimivva	$⊢ φ \to \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)$
471	470	adantr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)$
472	405 471	jctird	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \to (\exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) \land \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)))$
473		fveq2	$⊢ t = n \to 1^{st} (t) = 1^{st} (n)$
474	473	uneq1d	$⊢ t = n \to 1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\}$
475		fveq2	$⊢ t = n \to 2^{nd} (t) = 2^{nd} (n)$
476	475	uneq1d	$⊢ t = n \to 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}$
477	474 476	opeq12d	$⊢ t = n \to ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩$
478	477	eqeq2d	$⊢ t = n \to (k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩)$
479	478	reu4	$⊢ \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow (\exists t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n))$
480	58	rexrab	$⊢ \exists t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow \exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
481	480	anbi1i	$⊢ (\exists t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n)) \leftrightarrow (\exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) \land \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n))$
482	479 481	bitri	$⊢ \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow (\exists t \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (t) +_{f} ((2^{nd} (t) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (t) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \land k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) \land \forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \forall n \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ((k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \land k = ⟨1^{st} (n) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}⟩) \to t = n))$
483	472 482	syl6ibr	$⊢ (φ \land k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\})) \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \to \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
484	483	ralrimiva	$⊢ φ \to \forall k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \to \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
485		fveq2	$⊢ s = k \to 1^{st} (s) = 1^{st} (k)$
486		fveq2	$⊢ s = k \to 2^{nd} (s) = 2^{nd} (k)$
487	486	imaeq1d	$⊢ s = k \to 2^{nd} (s) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
488	487	xpeq1d	$⊢ s = k \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = 2^{nd} (k) [(1 \dots j)] \times \{1\}$
489	486	imaeq1d	$⊢ s = k \to 2^{nd} (s) [(j + 1 \dots M + 1)] = 2^{nd} (k) [(j + 1 \dots M + 1)]$
490	489	xpeq1d	$⊢ s = k \to 2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\} = 2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}$
491	488 490	uneq12d	$⊢ s = k \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}) = (2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\})$
492	485 491	oveq12d	$⊢ s = k \to 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\})) = 1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))$
493	492	uneq1d	$⊢ s = k \to (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})$
494	493	csbeq1d	$⊢ s = k \to ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B$
495	494	eqeq2d	$⊢ s = k \to (i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
496	495	rexbidv	$⊢ s = k \to (\exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
497	496	ralbidv	$⊢ s = k \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
498	485	fveq1d	$⊢ s = k \to 1^{st} (s) (M + 1) = 1^{st} (k) (M + 1)$
499	498	eqeq1d	$⊢ s = k \to (1^{st} (s) (M + 1) = 0 \leftrightarrow 1^{st} (k) (M + 1) = 0)$
500	486	fveq1d	$⊢ s = k \to 2^{nd} (s) (M + 1) = 2^{nd} (k) (M + 1)$
501	500	eqeq1d	$⊢ s = k \to (2^{nd} (s) (M + 1) = M + 1 \leftrightarrow 2^{nd} (k) (M + 1) = M + 1)$
502	497 499 501	3anbi123d	$⊢ s = k \to ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1) \leftrightarrow (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1))$
503	502	ralrab	$⊢ \forall k \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \leftrightarrow \forall k \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) ((\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (k) +_{f} ((2^{nd} (k) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (k) (M + 1) = 0 \land 2^{nd} (k) (M + 1) = M + 1) \to \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
504	484 503	sylibr	$⊢ φ \to \forall k \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩$
505		eqid	$⊢ (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟼ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) = (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟼ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
506	505	f1ompt	$⊢ (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟼ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) : \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \underset{1-1 onto}{⟶} \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \leftrightarrow (\forall t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩ \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \land \forall k \in \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \exists! t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} k = ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩)$
507	60 504 506	sylanbrc	$⊢ φ \to (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟼ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) : \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \underset{1-1 onto}{⟶} \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\}$
508		ovex	$⊢ {(0 ..^K)}^{(1 \dots M)} \in V$
509		ovex	$⊢ {(1 \dots M)}^{(1 \dots M)} \in V$
510		f1of	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to f : (1 \dots M) ⟶ (1 \dots M)$
511	510	ss2abi	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \subseteq \{f \| f : (1 \dots M) ⟶ (1 \dots M)\}$
512	68 68	mapval	$⊢ {(1 \dots M)}^{(1 \dots M)} = \{f \| f : (1 \dots M) ⟶ (1 \dots M)\}$
513	511 512	sseqtrri	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \subseteq {(1 \dots M)}^{(1 \dots M)}$
514	509 513	ssexi	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \in V$
515	508 514	xpex	$⊢ ({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \in V$
516	515	rabex	$⊢ \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \in V$
517	516	f1oen	$⊢ (t \in \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} ⟼ ⟨1^{st} (t) \cup \{⟨M + 1, 0⟩\}, 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}⟩) : \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \underset{1-1 onto}{⟶} \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\} \to \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \approx \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\}$
518	507 517	syl	$⊢ φ \to \{s \in (({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\}) \| \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B\} \approx \{s \in (({(0 ..^K)}^{(1 \dots M + 1)}) \times \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}) \| (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land 1^{st} (s) (M + 1) = 0 \land 2^{nd} (s) (M + 1) = M + 1)\}$

Metamath Proof Explorer

Theorem poimirlem4

Proof