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	imbitrrdi	$⊢ (φ \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	129	f1oeq3d	$⊢ ((φ \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))$
131	81 130	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)$
132	73	resex	$⊢ {2^{nd} (k) ↾}_{(1 \dots M)} \in V$
133		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))$
134	132 133	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)$
135	131 134	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)\}$
136	71 135	opelxpd	$⊢ ((φ \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)\})$
137	136	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)\})$
138		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))$
139	138	biancomi	$⊢ (\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)$
140	94	nnzd	$⊢ φ \to M + 1 \in ℤ$
141		uzid	$⊢ M + 1 \in ℤ \to M + 1 \in ℤ_{\geq (M + 1)}$
142		peano2uz	$⊢ M + 1 \in ℤ_{\geq (M + 1)} \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
143	140 141 142	3syl	$⊢ φ \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
144	3	nn0zd	$⊢ φ \to M \in ℤ$
145	1	nnzd	$⊢ φ \to N \in ℤ$
146		zltp1le	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow M + 1 \leq N)$
147		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
148		eluz	$⊢ (M + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
149	147 148	sylan	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
150	146 149	bitr4d	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
151	144 145 150	syl2anc	$⊢ φ \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
152	4 151	mpbid	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
153		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)$
154	143 152 153	syl2anc	$⊢ φ \to (M + 1 \dots N) = (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
155		fzsn	$⊢ M + 1 \in ℤ \to (M + 1 \dots M + 1) = \{M + 1\}$
156	140 155	syl	$⊢ φ \to (M + 1 \dots M + 1) = \{M + 1\}$
157	156	uneq1d	$⊢ φ \to (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
158	154 157	eqtrd	$⊢ φ \to (M + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
159	158	xpeq1d	$⊢ φ \to (M + 1 \dots N) \times \{0\} = (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\}$
160	159	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\})$
161		xpundir	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
162		ovex	$⊢ M + 1 \in V$
163		c0ex	$⊢ 0 \in V$
164	162 163	xpsn	$⊢ \{M + 1\} \times \{0\} = \{⟨M + 1, 0⟩\}$
165	164	uneq1i	$⊢ (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
166	161 165	eqtri	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
167	166	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\}))$
168		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\}))$
169	167 168	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\})$
170	160 169	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\})$
171	170	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\})$
172	162	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$
173	163	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$
174	110	eqcomd	$⊢ φ \to (1 \dots M) \cup \{M + 1\} = (1 \dots M + 1)$
175	174	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)$
176		fveq2	$⊢ n = M + 1 \to 1^{st} (k) (n) = 1^{st} (k) (M + 1)$
177		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)$
178	176 177	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)$
179		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$
180		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)]$
181	76 83 180	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)]$
182	181	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)]$
183		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
184	183	nn0red	$⊢ j \in (0 \dots M) \to j \in ℝ$
185	184	ltp1d	$⊢ j \in (0 \dots M) \to j < j + 1$
186		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
187	185 186	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
188	187	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = 2^{nd} (k) [\emptyset]$
189		ima0	$⊢ 2^{nd} (k) [\emptyset] = \emptyset$
190	188 189	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M + 1)] = \emptyset$
191	182 190	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$
192		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$
193	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)$
194		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
195		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
196	194 195	eleqtrdi	$⊢ j \in ℕ_{0} \to j + 1 \in ℤ_{\geq 1}$
197		fzss1	$⊢ j + 1 \in ℤ_{\geq 1} \to (j + 1 \dots M + 1) \subseteq (1 \dots M + 1)$
198	183 196 197	3syl	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \subseteq (1 \dots M + 1)$
199		elfzuz3	$⊢ j \in (0 \dots M) \to M \in ℤ_{\geq j}$
200		eluzp1p1	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq (j + 1)}$
201		eluzfz2	$⊢ M + 1 \in ℤ_{\geq (j + 1)} \to M + 1 \in (j + 1 \dots M + 1)$
202	199 200 201	3syl	$⊢ j \in (0 \dots M) \to M + 1 \in (j + 1 \dots M + 1)$
203	198 202	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))$
204		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)]$
205	204	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)]$
206	193 203 205	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)]$
207	192 206	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)]$
208		1ex	$⊢ 1 \in V$
209		fnconstg	$⊢ 1 \in V \to (2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)]$
210	208 209	ax-mp	$⊢ (2^{nd} (k) [(1 \dots j)] \times \{1\}) Fn 2^{nd} (k) [(1 \dots j)]$
211		fnconstg	$⊢ 0 \in V \to (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)]$
212	163 211	ax-mp	$⊢ (2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M + 1)]$
213		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)$
214	210 212 213	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)$
215	191 207 214	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)$
216	163	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$
217	207 216	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$
218	215 217	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$
219	218	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$
220	179 219	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$
221		00id	$⊢ 0 + 0 = 0$
222	220 221	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$
223	178 222	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$
224	172 173 175 223	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))$
225	224	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\})$
226	171 225	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\})$
227		elmapfn	$⊢ 1^{st} (k) \in ({(0 ..^K)}^{(1 \dots M + 1)}) \to 1^{st} (k) Fn (1 \dots M + 1)$
228	61 227	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)$
229		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)$
230	228 64 229	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)$
231	230	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)$
232		fnconstg	$⊢ 0 \in V \to (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)]$
233	163 232	ax-mp	$⊢ (2^{nd} (k) [(j + 1 \dots M)] \times \{0\}) Fn 2^{nd} (k) [(j + 1 \dots M)]$
234	210 233	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)])$
235		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)]$
236	76 83 235	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)]$
237		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
238	185 237	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
239	238	imaeq2d	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = 2^{nd} (k) [\emptyset]$
240	239 189	eqtrdi	$⊢ j \in (0 \dots M) \to 2^{nd} (k) [(1 \dots j) \cap (j + 1 \dots M)] = \emptyset$
241	236 240	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$
242		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)])$
243	234 241 242	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)])$
244	243	ad4ant24	$⊢ (((φ \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)])$
245	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\}$
246	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\}]$
247	183 194	syl	$⊢ j \in (0 \dots M) \to j + 1 \in ℕ$
248	247 195	eleqtrdi	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ_{\geq 1}$
249		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land M \in ℤ_{\geq j}) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
250	248 199 249	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
251	128 250	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)$
252	251	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)]$
253	246 252	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)]$
254	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)$
255	245 253 254	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)]$
256		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)]$
257	255 256	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)]$
258	257	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)]))$
259	244 258	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)$
260		fzss2	$⊢ M \in ℤ_{\geq j} \to (1 \dots j) \subseteq (1 \dots M)$
261		resima2	$⊢ (1 \dots j) \subseteq (1 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
262	199 260 261	3syl	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
263	262	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\}$
264	183 196	syl	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ_{\geq 1}$
265		fzss1	$⊢ j + 1 \in ℤ_{\geq 1} \to (j + 1 \dots M) \subseteq (1 \dots M)$
266		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)]$
267	264 265 266	3syl	$⊢ j \in (0 \dots M) \to ({2^{nd} (k) ↾}_{(1 \dots M)}) [(j + 1 \dots M)] = 2^{nd} (k) [(j + 1 \dots M)]$
268	267	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\}$
269	263 268	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\})$
270	269	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\})$
271	270	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))$
272	259 271	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)$
273		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$
274		inidm	$⊢ (1 \dots M) \cap (1 \dots M) = (1 \dots M)$
275		fvres	$⊢ n \in (1 \dots M) \to ({1^{st} (k) ↾}_{(1 \dots M)}) (n) = 1^{st} (k) (n)$
276	275	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)$
277		disjsn	$⊢ (1 \dots M) \cap \{M + 1\} = \emptyset \leftrightarrow \neg M + 1 \in (1 \dots M)$
278	122 277	sylibr	$⊢ φ \to (1 \dots M) \cap \{M + 1\} = \emptyset$
279	278	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$
280	259 279	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)$
281		fnconstg	$⊢ 0 \in V \to (\{M + 1\} \times \{0\}) Fn \{M + 1\}$
282	163 281	ax-mp	$⊢ (\{M + 1\} \times \{0\}) Fn \{M + 1\}$
283		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)$
284	282 283	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)$
285	284	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)$
286	280 285	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)$
287	247	nnzd	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ$
288	183	nn0cnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
289		pncan1	$⊢ j \in ℂ \to j + 1 - 1 = j$
290	288 289	syl	$⊢ j \in (0 \dots M) \to j + 1 - 1 = j$
291	290	fveq2d	$⊢ j \in (0 \dots M) \to ℤ_{\geq (j + 1 - 1)} = ℤ_{\geq j}$
292	199 291	eleqtrrd	$⊢ j \in (0 \dots M) \to M \in ℤ_{\geq (j + 1 - 1)}$
293		fzsuc2	$⊢ (j + 1 \in ℤ \land M \in ℤ_{\geq (j + 1 - 1)}) \to (j + 1 \dots M + 1) = (j + 1 \dots M) \cup \{M + 1\}$
294	287 292 293	syl2anc	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) = (j + 1 \dots M) \cup \{M + 1\}$
295	294	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\}]$
296		imaundi	$⊢ 2^{nd} (k) [(j + 1 \dots M) \cup \{M + 1\}] = 2^{nd} (k) [(j + 1 \dots M)] \cup 2^{nd} (k) [\{M + 1\}]$
297	295 296	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\}]$
298	297	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\}$
299		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\})$
300	298 299	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\})$
301	300	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\}))$
302		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\}))$
303	301 302	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\})$
304	303	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\})$
305	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\}$
306	305	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\})$
307	306	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\})$
308	304 307	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\})$
309	99	xpeq1d	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to \{2^{nd} (k) (M + 1)\} \times \{0\} = \{M + 1\} \times \{0\}$
310	309	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\})$
311	308 310	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\})$
312	311	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\})$
313	312	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)$
314	313	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)$
315	269	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)$
316	315	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)$
317	286 314 316	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)$
318	231 272 273 273 274 276 317	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))$
319	318	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\})$
320	319	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\})$
321	228	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)$
322	210 212	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)])$
323	181 190	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$
324		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)])$
325	322 323 324	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)])$
326		peano2uz	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq j}$
327	199 326	syl	$⊢ j \in (0 \dots M) \to M + 1 \in ℤ_{\geq j}$
328		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)$
329	264 327 328	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M + 1) = (1 \dots j) \cup (j + 1 \dots M + 1)$
330	329	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)]$
331		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)]$
332	330 331	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)]$
333	332 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)$
334	333	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))$
335	325 334	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)$
336		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$
337		inidm	$⊢ (1 \dots M + 1) \cap (1 \dots M + 1) = (1 \dots M + 1)$
338		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)$
339		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)$
340	321 335 336 336 337 338 339	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))$
341	340	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\})$
342	341	ad4ant24	$⊢ (((φ \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\})$
343	226 320 342	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\})$
344	343	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$
345	344	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)$
346	345	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)$
347	346	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)$
348	347	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)$
349	348	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$
350	139 349	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$
351		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)⟩$
352	351	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)⟩$
353		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)⟩\}$
354	228 96 353	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)⟩\}$
355	354	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)⟩\}$
356	125	reseq2d	$⊢ φ \to {1^{st} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {1^{st} (k) ↾}_{(1 \dots M)}$
357	356	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)}$
358		opeq2	$⊢ 1^{st} (k) (M + 1) = 0 \to ⟨M + 1, 1^{st} (k) (M + 1)⟩ = ⟨M + 1, 0⟩$
359	358	sneqd	$⊢ 1^{st} (k) (M + 1) = 0 \to \{⟨M + 1, 1^{st} (k) (M + 1)⟩\} = \{⟨M + 1, 0⟩\}$
360		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⟩\}$
361	357 359 360	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⟩\}$
362	355 361	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⟩\}$
363	362	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⟩\}$
364		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)⟩\}$
365	92 96 364	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)⟩\}$
366	365	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)⟩\}$
367	125	reseq2d	$⊢ φ \to {2^{nd} (k) ↾}_{((1 \dots M + 1) ∖ \{M + 1\})} = {2^{nd} (k) ↾}_{(1 \dots M)}$
368	367	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)}$
369		opeq2	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to ⟨M + 1, 2^{nd} (k) (M + 1)⟩ = ⟨M + 1, M + 1⟩$
370	369	sneqd	$⊢ 2^{nd} (k) (M + 1) = M + 1 \to \{⟨M + 1, 2^{nd} (k) (M + 1)⟩\} = \{⟨M + 1, M + 1⟩\}$
371		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⟩\}$
372	368 370 371	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⟩\}$
373	366 372	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⟩\}$
374	373	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⟩\}$
375	363 374	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⟩\}⟩$
376	352 375	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⟩\}⟩$
377	376	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⟩\}⟩$
378		fvex	$⊢ 1^{st} (k) \in V$
379	378	resex	$⊢ {1^{st} (k) ↾}_{(1 \dots M)} \in V$
380	379 132	op1std	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 1^{st} (t) = {1^{st} (k) ↾}_{(1 \dots M)}$
381	379 132	op2ndd	$⊢ t = ⟨{1^{st} (k) ↾}_{(1 \dots M)}, {2^{nd} (k) ↾}_{(1 \dots M)}⟩ \to 2^{nd} (t) = {2^{nd} (k) ↾}_{(1 \dots M)}$
382	381	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)]$
383	382	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\}$
384	381	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)]$
385	384	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\}$
386	383 385	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\})$
387	380 386	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\}))$
388	387	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\})$
389	388	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$
390	389	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)$
391	390	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)$
392	391	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)$
393	380	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⟩\}$
394	381	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⟩\}$
395	393 394	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⟩\}⟩$
396	395	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⟩\}⟩)$
397	392 396	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⟩\}⟩))$
398	397	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⟩\}⟩)$
399	137 350 377 398	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⟩\}⟩)$
400	399	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⟩\}⟩))$
401		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)\})$
402		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)\})$
403	401 402	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)\}))$
404		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⟩\}⟩$
405	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⟩\})$
406		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⟩\}$
407		difun2	$⊢ (1^{st} (t) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (t) ∖ \{⟨M + 1, 0⟩\}$
408		difun2	$⊢ (1^{st} (n) \cup \{⟨M + 1, 0⟩\}) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n) ∖ \{⟨M + 1, 0⟩\}$
409	406 407 408	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⟩\}$
410		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⟩\}$
411		difun2	$⊢ (2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\}$
412		difun2	$⊢ (2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\}$
413	410 411 412	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⟩\}$
414	409 413	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⟩\})$
415	405 414	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⟩\})$
416	404 415	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⟩\})$
417		elmapfn	$⊢ 1^{st} (t) \in ({(0 ..^K)}^{(1 \dots M)}) \to 1^{st} (t) Fn (1 \dots M)$
418		fnop	$⊢ (1^{st} (t) Fn (1 \dots M) \land ⟨M + 1, 0⟩ \in 1^{st} (t)) \to M + 1 \in (1 \dots M)$
419	418	ex	$⊢ 1^{st} (t) Fn (1 \dots M) \to (⟨M + 1, 0⟩ \in 1^{st} (t) \to M + 1 \in (1 \dots M))$
420	9 417 419	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))$
421	420 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))$
422	421	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)$
423		difsn	$⊢ \neg ⟨M + 1, 0⟩ \in 1^{st} (t) \to 1^{st} (t) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (t)$
424	422 423	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)$
425		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)})$
426		elmapfn	$⊢ 1^{st} (n) \in ({(0 ..^K)}^{(1 \dots M)}) \to 1^{st} (n) Fn (1 \dots M)$
427		fnop	$⊢ (1^{st} (n) Fn (1 \dots M) \land ⟨M + 1, 0⟩ \in 1^{st} (n)) \to M + 1 \in (1 \dots M)$
428	427	ex	$⊢ 1^{st} (n) Fn (1 \dots M) \to (⟨M + 1, 0⟩ \in 1^{st} (n) \to M + 1 \in (1 \dots M))$
429	425 426 428	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))$
430	429 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))$
431	430	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)$
432		difsn	$⊢ \neg ⟨M + 1, 0⟩ \in 1^{st} (n) \to 1^{st} (n) ∖ \{⟨M + 1, 0⟩\} = 1^{st} (n)$
433	431 432	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)$
434	424 433	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))$
435	434	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))$
436		f1ofn	$⊢ 2^{nd} (t) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to 2^{nd} (t) Fn (1 \dots M)$
437		fnop	$⊢ (2^{nd} (t) Fn (1 \dots M) \land ⟨M + 1, M + 1⟩ \in 2^{nd} (t)) \to M + 1 \in (1 \dots M)$
438	437	ex	$⊢ 2^{nd} (t) Fn (1 \dots M) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (t) \to M + 1 \in (1 \dots M))$
439	17 436 438	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))$
440	439 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))$
441	440	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)$
442		difsn	$⊢ \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (t) \to 2^{nd} (t) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (t)$
443	441 442	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)$
444		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)\}$
445		fvex	$⊢ 2^{nd} (n) \in V$
446		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))$
447	445 446	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)$
448	444 447	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)$
449		f1ofn	$⊢ 2^{nd} (n) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to 2^{nd} (n) Fn (1 \dots M)$
450		fnop	$⊢ (2^{nd} (n) Fn (1 \dots M) \land ⟨M + 1, M + 1⟩ \in 2^{nd} (n)) \to M + 1 \in (1 \dots M)$
451	450	ex	$⊢ 2^{nd} (n) Fn (1 \dots M) \to (⟨M + 1, M + 1⟩ \in 2^{nd} (n) \to M + 1 \in (1 \dots M))$
452	448 449 451	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))$
453	452 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))$
454	453	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)$
455		difsn	$⊢ \neg ⟨M + 1, M + 1⟩ \in 2^{nd} (n) \to 2^{nd} (n) ∖ \{⟨M + 1, M + 1⟩\} = 2^{nd} (n)$
456	454 455	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)$
457	443 456	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))$
458	457	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))$
459	435 458	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)))$
460		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)$
461	460	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)$
462	459 461	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)$
463	416 462	imbitrid	$⊢ (φ \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)$
464	403 463	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)$
465	464	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)$
466	465	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)$
467	400 466	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)))$
468		fveq2	$⊢ t = n \to 1^{st} (t) = 1^{st} (n)$
469	468	uneq1d	$⊢ t = n \to 1^{st} (t) \cup \{⟨M + 1, 0⟩\} = 1^{st} (n) \cup \{⟨M + 1, 0⟩\}$
470		fveq2	$⊢ t = n \to 2^{nd} (t) = 2^{nd} (n)$
471	470	uneq1d	$⊢ t = n \to 2^{nd} (t) \cup \{⟨M + 1, M + 1⟩\} = 2^{nd} (n) \cup \{⟨M + 1, M + 1⟩\}$
472	469 471	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⟩\}⟩$
473	472	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⟩\}⟩)$
474	473	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))$
475	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⟩\}⟩)$
476	475	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))$
477	474 476	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))$
478	467 477	imbitrrdi	$⊢ (φ \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⟩\}⟩)$
479	478	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⟩\}⟩)$
480		fveq2	$⊢ s = k \to 1^{st} (s) = 1^{st} (k)$
481		fveq2	$⊢ s = k \to 2^{nd} (s) = 2^{nd} (k)$
482	481	imaeq1d	$⊢ s = k \to 2^{nd} (s) [(1 \dots j)] = 2^{nd} (k) [(1 \dots j)]$
483	482	xpeq1d	$⊢ s = k \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = 2^{nd} (k) [(1 \dots j)] \times \{1\}$
484	481	imaeq1d	$⊢ s = k \to 2^{nd} (s) [(j + 1 \dots M + 1)] = 2^{nd} (k) [(j + 1 \dots M + 1)]$
485	484	xpeq1d	$⊢ s = k \to 2^{nd} (s) [(j + 1 \dots M + 1)] \times \{0\} = 2^{nd} (k) [(j + 1 \dots M + 1)] \times \{0\}$
486	483 485	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\})$
487	480 486	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\}))$
488	487	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\})$
489	488	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$
490	489	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)$
491	490	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)$
492	491	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)$
493	480	fveq1d	$⊢ s = k \to 1^{st} (s) (M + 1) = 1^{st} (k) (M + 1)$
494	493	eqeq1d	$⊢ s = k \to (1^{st} (s) (M + 1) = 0 \leftrightarrow 1^{st} (k) (M + 1) = 0)$
495	481	fveq1d	$⊢ s = k \to 2^{nd} (s) (M + 1) = 2^{nd} (k) (M + 1)$
496	495	eqeq1d	$⊢ s = k \to (2^{nd} (s) (M + 1) = M + 1 \leftrightarrow 2^{nd} (k) (M + 1) = M + 1)$
497	492 494 496	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))$
498	497	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⟩\}⟩)$
499	479 498	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⟩\}⟩$
500		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⟩\}⟩)$
501	500	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⟩\}⟩)$
502	60 499 501	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)\}$
503		ovex	$⊢ {(0 ..^K)}^{(1 \dots M)} \in V$
504		ovex	$⊢ {(1 \dots M)}^{(1 \dots M)} \in V$
505		f1of	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to f : (1 \dots M) ⟶ (1 \dots M)$
506	505	ss2abi	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \subseteq \{f \| f : (1 \dots M) ⟶ (1 \dots M)\}$
507	68 68	mapval	$⊢ {(1 \dots M)}^{(1 \dots M)} = \{f \| f : (1 \dots M) ⟶ (1 \dots M)\}$
508	506 507	sseqtrri	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \subseteq {(1 \dots M)}^{(1 \dots M)}$
509	504 508	ssexi	$⊢ \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \in V$
510	503 509	xpex	$⊢ ({(0 ..^K)}^{(1 \dots M)}) \times \{f \| f : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)\} \in V$
511	510	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$
512	511	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)\}$
513	502 512	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