poimirlem3

Description: Lemma for poimir to add an interior point to an admissible face on the back face of the 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$
	poimirlem3.4	$⊢ φ \to T : (1 \dots M) ⟶ (0 ..^K)$
	poimirlem3.5	$⊢ φ \to U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
Assertion	poimirlem3	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to (⟨T \cup \{⟨M + 1, 0⟩\}, U \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 = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (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		poimirlem3.4	$⊢ φ \to T : (1 \dots M) ⟶ (0 ..^K)$
6		poimirlem3.5	$⊢ φ \to U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
7		ovexd	$⊢ (φ \land j \in (0 \dots M)) \to (1 \dots M) \in V$
8	5	ffnd	$⊢ φ \to T Fn (1 \dots M)$
9	8	adantr	$⊢ (φ \land j \in (0 \dots M)) \to T Fn (1 \dots M)$
10		1ex	$⊢ 1 \in V$
11		fnconstg	$⊢ 1 \in V \to (U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)]$
12	10 11	ax-mp	$⊢ (U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)]$
13		c0ex	$⊢ 0 \in V$
14		fnconstg	$⊢ 0 \in V \to (U [(j + 1 \dots M)] \times \{0\}) Fn U [(j + 1 \dots M)]$
15	13 14	ax-mp	$⊢ (U [(j + 1 \dots M)] \times \{0\}) Fn U [(j + 1 \dots M)]$
16	12 15	pm3.2i	$⊢ ((U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)] \land (U [(j + 1 \dots M)] \times \{0\}) Fn U [(j + 1 \dots M)])$
17		dff1o3	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \leftrightarrow (U : (1 \dots M) \underset{onto}{⟶} (1 \dots M) \land Fun U^{-1})$
18	17	simprbi	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to Fun U^{-1}$
19		imain	$⊢ Fun U^{-1} \to U [(1 \dots j) \cap (j + 1 \dots M)] = U [(1 \dots j)] \cap U [(j + 1 \dots M)]$
20	6 18 19	3syl	$⊢ φ \to U [(1 \dots j) \cap (j + 1 \dots M)] = U [(1 \dots j)] \cap U [(j + 1 \dots M)]$
21		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
22	21	nn0red	$⊢ j \in (0 \dots M) \to j \in ℝ$
23	22	ltp1d	$⊢ j \in (0 \dots M) \to j < j + 1$
24		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
25	23 24	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M) = \emptyset$
26	25	imaeq2d	$⊢ j \in (0 \dots M) \to U [(1 \dots j) \cap (j + 1 \dots M)] = U [\emptyset]$
27		ima0	$⊢ U [\emptyset] = \emptyset$
28	26 27	eqtrdi	$⊢ j \in (0 \dots M) \to U [(1 \dots j) \cap (j + 1 \dots M)] = \emptyset$
29	20 28	sylan9req	$⊢ (φ \land j \in (0 \dots M)) \to U [(1 \dots j)] \cap U [(j + 1 \dots M)] = \emptyset$
30		fnun	$⊢ (((U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)] \land (U [(j + 1 \dots M)] \times \{0\}) Fn U [(j + 1 \dots M)]) \land U [(1 \dots j)] \cap U [(j + 1 \dots M)] = \emptyset) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) Fn (U [(1 \dots j)] \cup U [(j + 1 \dots M)])$
31	16 29 30	sylancr	$⊢ (φ \land j \in (0 \dots M)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) Fn (U [(1 \dots j)] \cup U [(j + 1 \dots M)])$
32		imaundi	$⊢ U [(1 \dots j) \cup (j + 1 \dots M)] = U [(1 \dots j)] \cup U [(j + 1 \dots M)]$
33		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
34		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
35	33 34	eleqtrdi	$⊢ j \in ℕ_{0} \to j + 1 \in ℤ_{\geq 1}$
36	21 35	syl	$⊢ j \in (0 \dots M) \to j + 1 \in ℤ_{\geq 1}$
37		elfzuz3	$⊢ j \in (0 \dots M) \to M \in ℤ_{\geq j}$
38		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land M \in ℤ_{\geq j}) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
39	36 37 38	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M) = (1 \dots j) \cup (j + 1 \dots M)$
40	39	eqcomd	$⊢ j \in (0 \dots M) \to (1 \dots j) \cup (j + 1 \dots M) = (1 \dots M)$
41	40	imaeq2d	$⊢ j \in (0 \dots M) \to U [(1 \dots j) \cup (j + 1 \dots M)] = U [(1 \dots M)]$
42		f1ofo	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to U : (1 \dots M) \underset{onto}{⟶} (1 \dots M)$
43		foima	$⊢ U : (1 \dots M) \underset{onto}{⟶} (1 \dots M) \to U [(1 \dots M)] = (1 \dots M)$
44	6 42 43	3syl	$⊢ φ \to U [(1 \dots M)] = (1 \dots M)$
45	41 44	sylan9eqr	$⊢ (φ \land j \in (0 \dots M)) \to U [(1 \dots j) \cup (j + 1 \dots M)] = (1 \dots M)$
46	32 45	eqtr3id	$⊢ (φ \land j \in (0 \dots M)) \to U [(1 \dots j)] \cup U [(j + 1 \dots M)] = (1 \dots M)$
47	46	fneq2d	$⊢ (φ \land j \in (0 \dots M)) \to (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) Fn (U [(1 \dots j)] \cup U [(j + 1 \dots M)]) \leftrightarrow ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M))$
48	31 47	mpbid	$⊢ (φ \land j \in (0 \dots M)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) Fn (1 \dots M)$
49	7 9 48	offvalfv	$⊢ (φ \land j \in (0 \dots M)) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n))$
50		nn0p1nn	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ$
51	3 50	syl	$⊢ φ \to M + 1 \in ℕ$
52	51	nnzd	$⊢ φ \to M + 1 \in ℤ$
53		uzid	$⊢ M + 1 \in ℤ \to M + 1 \in ℤ_{\geq (M + 1)}$
54		peano2uz	$⊢ M + 1 \in ℤ_{\geq (M + 1)} \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
55	52 53 54	3syl	$⊢ φ \to M + 1 + 1 \in ℤ_{\geq (M + 1)}$
56	3	nn0zd	$⊢ φ \to M \in ℤ$
57	1	nnzd	$⊢ φ \to N \in ℤ$
58		zltp1le	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow M + 1 \leq N)$
59		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
60		eluz	$⊢ (M + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
61	59 60	sylan	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow M + 1 \leq N)$
62	58 61	bitr4d	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
63	56 57 62	syl2anc	$⊢ φ \to (M < N \leftrightarrow N \in ℤ_{\geq (M + 1)})$
64	4 63	mpbid	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
65		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)$
66	55 64 65	syl2anc	$⊢ φ \to (M + 1 \dots N) = (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
67		fzsn	$⊢ M + 1 \in ℤ \to (M + 1 \dots M + 1) = \{M + 1\}$
68	52 67	syl	$⊢ φ \to (M + 1 \dots M + 1) = \{M + 1\}$
69	68	uneq1d	$⊢ φ \to (M + 1 \dots M + 1) \cup (M + 1 + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
70	66 69	eqtrd	$⊢ φ \to (M + 1 \dots N) = \{M + 1\} \cup (M + 1 + 1 \dots N)$
71	70	xpeq1d	$⊢ φ \to (M + 1 \dots N) \times \{0\} = (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\}$
72		xpundir	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
73		ovex	$⊢ M + 1 \in V$
74	73 13	xpsn	$⊢ \{M + 1\} \times \{0\} = \{⟨M + 1, 0⟩\}$
75	74	uneq1i	$⊢ (\{M + 1\} \times \{0\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
76	72 75	eqtri	$⊢ (\{M + 1\} \cup (M + 1 + 1 \dots N)) \times \{0\} = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
77	71 76	eqtrdi	$⊢ φ \to (M + 1 \dots N) \times \{0\} = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
78	77	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (M + 1 \dots N) \times \{0\} = \{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\})$
79	49 78	uneq12d	$⊢ (φ \land j \in (0 \dots M)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup (\{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\}))$
80		unass	$⊢ ((n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\}) = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup (\{⟨M + 1, 0⟩\} \cup ((M + 1 + 1 \dots N) \times \{0\}))$
81	79 80	eqtr4di	$⊢ (φ \land j \in (0 \dots M)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = ((n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
82		ovexd	$⊢ (φ \land j \in (0 \dots M)) \to (1 \dots M + 1) \in V$
83	3	nn0red	$⊢ φ \to M \in ℝ$
84	83	ltp1d	$⊢ φ \to M < M + 1$
85	51	nnred	$⊢ φ \to M + 1 \in ℝ$
86	83 85	ltnled	$⊢ φ \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
87	84 86	mpbid	$⊢ φ \to \neg M + 1 \leq M$
88		elfzle2	$⊢ M + 1 \in (1 \dots M) \to M + 1 \leq M$
89	87 88	nsyl	$⊢ φ \to \neg M + 1 \in (1 \dots M)$
90		disjsn	$⊢ (1 \dots M) \cap \{M + 1\} = \emptyset \leftrightarrow \neg M + 1 \in (1 \dots M)$
91	89 90	sylibr	$⊢ φ \to (1 \dots M) \cap \{M + 1\} = \emptyset$
92		eqid	$⊢ \{⟨M + 1, 0⟩\} = \{⟨M + 1, 0⟩\}$
93	73 13	fsn	$⊢ \{⟨M + 1, 0⟩\} : \{M + 1\} ⟶ \{0\} \leftrightarrow \{⟨M + 1, 0⟩\} = \{⟨M + 1, 0⟩\}$
94	92 93	mpbir	$⊢ \{⟨M + 1, 0⟩\} : \{M + 1\} ⟶ \{0\}$
95		fun	$⊢ ((T : (1 \dots M) ⟶ (0 ..^K) \land \{⟨M + 1, 0⟩\} : \{M + 1\} ⟶ \{0\}) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M) \cup \{M + 1\} ⟶ (0 ..^K) \cup \{0\}$
96	94 95	mpanl2	$⊢ (T : (1 \dots M) ⟶ (0 ..^K) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M) \cup \{M + 1\} ⟶ (0 ..^K) \cup \{0\}$
97	5 91 96	syl2anc	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M) \cup \{M + 1\} ⟶ (0 ..^K) \cup \{0\}$
98		1z	$⊢ 1 \in ℤ$
99		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
100		1m1e0	$⊢ 1 - 1 = 0$
101	100	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
102	99 101	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
103	3 102	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (1 - 1)}$
104		fzsuc2	$⊢ (1 \in ℤ \land M \in ℤ_{\geq (1 - 1)}) \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
105	98 103 104	sylancr	$⊢ φ \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
106	105	eqcomd	$⊢ φ \to (1 \dots M) \cup \{M + 1\} = (1 \dots M + 1)$
107		lbfzo0	$⊢ 0 \in (0 ..^K) \leftrightarrow K \in ℕ$
108	2 107	sylibr	$⊢ φ \to 0 \in (0 ..^K)$
109	108	snssd	$⊢ φ \to \{0\} \subseteq (0 ..^K)$
110		ssequn2	$⊢ \{0\} \subseteq (0 ..^K) \leftrightarrow (0 ..^K) \cup \{0\} = (0 ..^K)$
111	109 110	sylib	$⊢ φ \to (0 ..^K) \cup \{0\} = (0 ..^K)$
112	106 111	feq23d	$⊢ φ \to ((T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M) \cup \{M + 1\} ⟶ (0 ..^K) \cup \{0\} \leftrightarrow (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M + 1) ⟶ (0 ..^K))$
113	97 112	mpbid	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M + 1) ⟶ (0 ..^K)$
114	113	ffnd	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) Fn (1 \dots M + 1)$
115	114	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) Fn (1 \dots M + 1)$
116		fnconstg	$⊢ 1 \in V \to ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)]$
117	10 116	ax-mp	$⊢ ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)]$
118		fnconstg	$⊢ 0 \in V \to ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
119	13 118	ax-mp	$⊢ ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
120	117 119	pm3.2i	$⊢ (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \land ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)])$
121	73 73	f1osn	$⊢ \{⟨M + 1, M + 1⟩\} : \{M + 1\} \underset{1-1 onto}{⟶} \{M + 1\}$
122		f1oun	$⊢ ((U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \land \{⟨M + 1, M + 1⟩\} : \{M + 1\} \underset{1-1 onto}{⟶} \{M + 1\}) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land (1 \dots M) \cap \{M + 1\} = \emptyset)) \to (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\}$
123	121 122	mpanl2	$⊢ (U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land (1 \dots M) \cap \{M + 1\} = \emptyset)) \to (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\}$
124	6 91 91 123	syl12anc	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\}$
125		dff1o3	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\} \leftrightarrow ((U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{onto}{⟶} (1 \dots M) \cup \{M + 1\} \land Fun {(U \cup \{⟨M + 1, M + 1⟩\})}^{-1})$
126	125	simprbi	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\} \to Fun {(U \cup \{⟨M + 1, M + 1⟩\})}^{-1}$
127		imain	$⊢ Fun {(U \cup \{⟨M + 1, M + 1⟩\})}^{-1} \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cap (j + 1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
128	124 126 127	3syl	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cap (j + 1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
129		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
130	23 129	syl	$⊢ j \in (0 \dots M) \to (1 \dots j) \cap (j + 1 \dots M + 1) = \emptyset$
131	130	imaeq2d	$⊢ j \in (0 \dots M) \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cap (j + 1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [\emptyset]$
132		ima0	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [\emptyset] = \emptyset$
133	131 132	eqtrdi	$⊢ j \in (0 \dots M) \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cap (j + 1 \dots M + 1)] = \emptyset$
134	128 133	sylan9req	$⊢ (φ \land j \in (0 \dots M)) \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] = \emptyset$
135		fnun	$⊢ ((((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \land ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]) \land (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] = \emptyset) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) Fn ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cup (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)])$
136	120 134 135	sylancr	$⊢ (φ \land j \in (0 \dots M)) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) Fn ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cup (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)])$
137		f1ofo	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\} \to (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{onto}{⟶} (1 \dots M) \cup \{M + 1\}$
138		foima	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{onto}{⟶} (1 \dots M) \cup \{M + 1\} \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M) \cup \{M + 1\}] = (1 \dots M) \cup \{M + 1\}$
139	124 137 138	3syl	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M) \cup \{M + 1\}] = (1 \dots M) \cup \{M + 1\}$
140	105	imaeq2d	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M) \cup \{M + 1\}]$
141	139 140 105	3eqtr4d	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M + 1)] = (1 \dots M + 1)$
142		peano2uz	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq j}$
143	37 142	syl	$⊢ j \in (0 \dots M) \to M + 1 \in ℤ_{\geq j}$
144		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)$
145	36 143 144	syl2anc	$⊢ j \in (0 \dots M) \to (1 \dots M + 1) = (1 \dots j) \cup (j + 1 \dots M + 1)$
146	145	imaeq2d	$⊢ j \in (0 \dots M) \to (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cup (j + 1 \dots M + 1)]$
147	141 146	sylan9req	$⊢ (φ \land j \in (0 \dots M)) \to (1 \dots M + 1) = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cup (j + 1 \dots M + 1)]$
148		imaundi	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j) \cup (j + 1 \dots M + 1)] = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cup (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
149	147 148	eqtrdi	$⊢ (φ \land j \in (0 \dots M)) \to (1 \dots M + 1) = (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cup (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
150	149	fneq2d	$⊢ (φ \land j \in (0 \dots M)) \to ((((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) Fn (1 \dots M + 1) \leftrightarrow (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) Fn ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cup (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]))$
151	136 150	mpbird	$⊢ (φ \land j \in (0 \dots M)) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) Fn (1 \dots M + 1)$
152	82 115 151	offvalfv	$⊢ (φ \land j \in (0 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) = (n \in (1 \dots M + 1) ⟼ (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n))$
153		imadmrn	$⊢ (\{M + 1\} \times \{M + 1\}) [dom (\{M + 1\} \times \{M + 1\})] = ran (\{M + 1\} \times \{M + 1\})$
154	73 73	xpsn	$⊢ \{M + 1\} \times \{M + 1\} = \{⟨M + 1, M + 1⟩\}$
155	154	imaeq1i	$⊢ (\{M + 1\} \times \{M + 1\}) [dom (\{M + 1\} \times \{M + 1\})] = \{⟨M + 1, M + 1⟩\} [dom (\{M + 1\} \times \{M + 1\})]$
156		dmxpid	$⊢ dom (\{M + 1\} \times \{M + 1\}) = \{M + 1\}$
157	156	imaeq2i	$⊢ \{⟨M + 1, M + 1⟩\} [dom (\{M + 1\} \times \{M + 1\})] = \{⟨M + 1, M + 1⟩\} [\{M + 1\}]$
158	155 157	eqtri	$⊢ (\{M + 1\} \times \{M + 1\}) [dom (\{M + 1\} \times \{M + 1\})] = \{⟨M + 1, M + 1⟩\} [\{M + 1\}]$
159		rnxpid	$⊢ ran (\{M + 1\} \times \{M + 1\}) = \{M + 1\}$
160	153 158 159	3eqtr3ri	$⊢ \{M + 1\} = \{⟨M + 1, M + 1⟩\} [\{M + 1\}]$
161		eluzp1p1	$⊢ M \in ℤ_{\geq j} \to M + 1 \in ℤ_{\geq (j + 1)}$
162		eluzfz2	$⊢ M + 1 \in ℤ_{\geq (j + 1)} \to M + 1 \in (j + 1 \dots M + 1)$
163	37 161 162	3syl	$⊢ j \in (0 \dots M) \to M + 1 \in (j + 1 \dots M + 1)$
164	163	snssd	$⊢ j \in (0 \dots M) \to \{M + 1\} \subseteq (j + 1 \dots M + 1)$
165		imass2	$⊢ \{M + 1\} \subseteq (j + 1 \dots M + 1) \to \{⟨M + 1, M + 1⟩\} [\{M + 1\}] \subseteq \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
166	164 165	syl	$⊢ j \in (0 \dots M) \to \{⟨M + 1, M + 1⟩\} [\{M + 1\}] \subseteq \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
167	160 166	eqsstrid	$⊢ j \in (0 \dots M) \to \{M + 1\} \subseteq \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
168	73	snid	$⊢ M + 1 \in \{M + 1\}$
169		ssel	$⊢ \{M + 1\} \subseteq \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \to (M + 1 \in \{M + 1\} \to M + 1 \in \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)])$
170	167 168 169	mpisyl	$⊢ j \in (0 \dots M) \to M + 1 \in \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
171		elun2	$⊢ M + 1 \in \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \to M + 1 \in (U [(j + 1 \dots M + 1)] \cup \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)])$
172	170 171	syl	$⊢ j \in (0 \dots M) \to M + 1 \in (U [(j + 1 \dots M + 1)] \cup \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)])$
173		imaundir	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] = U [(j + 1 \dots M + 1)] \cup \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
174	172 173	eleqtrrdi	$⊢ j \in (0 \dots M) \to M + 1 \in (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
175	174	adantl	$⊢ (φ \land j \in (0 \dots M)) \to M + 1 \in (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]$
176	13	a1i	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in V$
177	106	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (1 \dots M) \cup \{M + 1\} = (1 \dots M + 1)$
178		fveq2	$⊢ n = M + 1 \to (T \cup \{⟨M + 1, 0⟩\}) (n) = (T \cup \{⟨M + 1, 0⟩\}) (M + 1)$
179	73 13	fnsn	$⊢ \{⟨M + 1, 0⟩\} Fn \{M + 1\}$
180		fvun2	$⊢ (T Fn (1 \dots M) \land \{⟨M + 1, 0⟩\} Fn \{M + 1\} \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land M + 1 \in \{M + 1\})) \to (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = \{⟨M + 1, 0⟩\} (M + 1)$
181	179 180	mp3an2	$⊢ (T Fn (1 \dots M) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land M + 1 \in \{M + 1\})) \to (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = \{⟨M + 1, 0⟩\} (M + 1)$
182	168 181	mpanr2	$⊢ (T Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \to (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = \{⟨M + 1, 0⟩\} (M + 1)$
183	8 91 182	syl2anc	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = \{⟨M + 1, 0⟩\} (M + 1)$
184	73 13	fvsn	$⊢ \{⟨M + 1, 0⟩\} (M + 1) = 0$
185	183 184	eqtrdi	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0$
186	178 185	sylan9eqr	$⊢ (φ \land n = M + 1) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = 0$
187	186	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land n = M + 1) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = 0$
188		fveq2	$⊢ n = M + 1 \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1)$
189		fvun2	$⊢ (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \land ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) Fn (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \land ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] = \emptyset \land M + 1 \in (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)])) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
190	117 119 189	mp3an12	$⊢ ((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \cap (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] = \emptyset \land M + 1 \in (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)]) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
191	134 175 190	syl2anc	$⊢ (φ \land j \in (0 \dots M)) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1)$
192	13	fvconst2	$⊢ M + 1 \in (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \to ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1) = 0$
193	174 192	syl	$⊢ j \in (0 \dots M) \to ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1) = 0$
194	193	adantl	$⊢ (φ \land j \in (0 \dots M)) \to ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) (M + 1) = 0$
195	191 194	eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (M + 1) = 0$
196	188 195	sylan9eqr	$⊢ ((φ \land j \in (0 \dots M)) \land n = M + 1) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = 0$
197	187 196	oveq12d	$⊢ ((φ \land j \in (0 \dots M)) \land n = M + 1) \to (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = 0 + 0$
198		00id	$⊢ 0 + 0 = 0$
199	197 198	eqtrdi	$⊢ ((φ \land j \in (0 \dots M)) \land n = M + 1) \to (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = 0$
200	175 176 177 199	fmptapd	$⊢ (φ \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\} = (n \in (1 \dots M + 1) ⟼ (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n))$
201	8 91	jca	$⊢ φ \to (T Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset)$
202		fvun1	$⊢ (T Fn (1 \dots M) \land \{⟨M + 1, 0⟩\} Fn \{M + 1\} \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land n \in (1 \dots M))) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = T (n)$
203	179 202	mp3an2	$⊢ (T Fn (1 \dots M) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land n \in (1 \dots M))) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = T (n)$
204	203	anassrs	$⊢ ((T Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \land n \in (1 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = T (n)$
205	201 204	sylan	$⊢ (φ \land n \in (1 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = T (n)$
206	205	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) (n) = T (n)$
207		fvres	$⊢ n \in (1 \dots M) \to ({(((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)}) (n) = (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n)$
208	207	eqcomd	$⊢ n \in (1 \dots M) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = ({(((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)}) (n)$
209		resundir	$⊢ {(((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)} = ({((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) \cup ({((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)})$
210		relxp	$⊢ Rel (U [(1 \dots j)] \times \{1\})$
211		dmxpss	$⊢ dom (U [(1 \dots j)] \times \{1\}) \subseteq U [(1 \dots j)]$
212		imassrn	$⊢ U [(1 \dots j)] \subseteq ran U$
213	211 212	sstri	$⊢ dom (U [(1 \dots j)] \times \{1\}) \subseteq ran U$
214		f1of	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to U : (1 \dots M) ⟶ (1 \dots M)$
215		frn	$⊢ U : (1 \dots M) ⟶ (1 \dots M) \to ran U \subseteq (1 \dots M)$
216	6 214 215	3syl	$⊢ φ \to ran U \subseteq (1 \dots M)$
217	213 216	sstrid	$⊢ φ \to dom (U [(1 \dots j)] \times \{1\}) \subseteq (1 \dots M)$
218		relssres	$⊢ (Rel (U [(1 \dots j)] \times \{1\}) \land dom (U [(1 \dots j)] \times \{1\}) \subseteq (1 \dots M)) \to {(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = U [(1 \dots j)] \times \{1\}$
219	210 217 218	sylancr	$⊢ φ \to {(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = U [(1 \dots j)] \times \{1\}$
220	219	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = U [(1 \dots j)] \times \{1\}$
221		imassrn	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \subseteq ran \{⟨M + 1, M + 1⟩\}$
222	73	rnsnop	$⊢ ran \{⟨M + 1, M + 1⟩\} = \{M + 1\}$
223	221 222	sseqtri	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \subseteq \{M + 1\}$
224		ssrin	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \subseteq \{M + 1\} \to \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) \subseteq \{M + 1\} \cap (1 \dots M)$
225	223 224	ax-mp	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) \subseteq \{M + 1\} \cap (1 \dots M)$
226		incom	$⊢ \{M + 1\} \cap (1 \dots M) = (1 \dots M) \cap \{M + 1\}$
227	226 91	eqtrid	$⊢ φ \to \{M + 1\} \cap (1 \dots M) = \emptyset$
228	225 227	sseqtrid	$⊢ φ \to \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) \subseteq \emptyset$
229		ss0	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) \subseteq \emptyset \to \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) = \emptyset$
230	228 229	syl	$⊢ φ \to \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) = \emptyset$
231		fnconstg	$⊢ 1 \in V \to (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) Fn \{⟨M + 1, M + 1⟩\} [(1 \dots j)]$
232		fnresdisj	$⊢ (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) Fn \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \to (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) = \emptyset \leftrightarrow {(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = \emptyset)$
233	10 231 232	mp2b	$⊢ \{⟨M + 1, M + 1⟩\} [(1 \dots j)] \cap (1 \dots M) = \emptyset \leftrightarrow {(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = \emptyset$
234	230 233	sylib	$⊢ φ \to {(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = \emptyset$
235	234	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = \emptyset$
236	220 235	uneq12d	$⊢ (φ \land j \in (0 \dots M)) \to ({(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) = (U [(1 \dots j)] \times \{1\}) \cup \emptyset$
237		imaundir	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] = U [(1 \dots j)] \cup \{⟨M + 1, M + 1⟩\} [(1 \dots j)]$
238	237	xpeq1i	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\} = (U [(1 \dots j)] \cup \{⟨M + 1, M + 1⟩\} [(1 \dots j)]) \times \{1\}$
239		xpundir	$⊢ (U [(1 \dots j)] \cup \{⟨M + 1, M + 1⟩\} [(1 \dots j)]) \times \{1\} = (U [(1 \dots j)] \times \{1\}) \cup (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\})$
240	238 239	eqtri	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\} = (U [(1 \dots j)] \times \{1\}) \cup (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\})$
241	240	reseq1i	$⊢ {((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = {((U [(1 \dots j)] \times \{1\}) \cup (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\})) ↾}_{(1 \dots M)}$
242		resundir	$⊢ {((U [(1 \dots j)] \times \{1\}) \cup (\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\})) ↾}_{(1 \dots M)} = ({(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)})$
243	241 242	eqtr2i	$⊢ ({(U [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) = {((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}$
244		un0	$⊢ (U [(1 \dots j)] \times \{1\}) \cup \emptyset = U [(1 \dots j)] \times \{1\}$
245	236 243 244	3eqtr3g	$⊢ (φ \land j \in (0 \dots M)) \to {((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)} = U [(1 \dots j)] \times \{1\}$
246		f1odm	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to dom U = (1 \dots M)$
247	6 246	syl	$⊢ φ \to dom U = (1 \dots M)$
248	247	ineq2d	$⊢ φ \to (j + 1 \dots M + 1) \cap dom U = (j + 1 \dots M + 1) \cap (1 \dots M)$
249	248	reseq2d	$⊢ φ \to {U ↾}_{((j + 1 \dots M + 1) \cap dom U)} = {U ↾}_{((j + 1 \dots M + 1) \cap (1 \dots M))}$
250		resindm	$⊢ {U ↾}_{((j + 1 \dots M + 1) \cap dom U)} = {U ↾}_{(j + 1 \dots M + 1)}$
251	249 250	eqtr3di	$⊢ φ \to {U ↾}_{((j + 1 \dots M + 1) \cap (1 \dots M))} = {U ↾}_{(j + 1 \dots M + 1)}$
252	39	ineq2d	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \cap (1 \dots M) = (j + 1 \dots M + 1) \cap ((1 \dots j) \cup (j + 1 \dots M))$
253		fzssp1	$⊢ (j + 1 \dots M) \subseteq (j + 1 \dots M + 1)$
254		sseqin2	$⊢ (j + 1 \dots M) \subseteq (j + 1 \dots M + 1) \leftrightarrow (j + 1 \dots M + 1) \cap (j + 1 \dots M) = (j + 1 \dots M)$
255	253 254	mpbi	$⊢ (j + 1 \dots M + 1) \cap (j + 1 \dots M) = (j + 1 \dots M)$
256	255	a1i	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \cap (j + 1 \dots M) = (j + 1 \dots M)$
257		incom	$⊢ (j + 1 \dots M + 1) \cap (1 \dots j) = (1 \dots j) \cap (j + 1 \dots M + 1)$
258	257 130	eqtrid	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \cap (1 \dots j) = \emptyset$
259	256 258	uneq12d	$⊢ j \in (0 \dots M) \to ((j + 1 \dots M + 1) \cap (j + 1 \dots M)) \cup ((j + 1 \dots M + 1) \cap (1 \dots j)) = (j + 1 \dots M) \cup \emptyset$
260		uncom	$⊢ ((j + 1 \dots M + 1) \cap (j + 1 \dots M)) \cup ((j + 1 \dots M + 1) \cap (1 \dots j)) = ((j + 1 \dots M + 1) \cap (1 \dots j)) \cup ((j + 1 \dots M + 1) \cap (j + 1 \dots M))$
261		indi	$⊢ (j + 1 \dots M + 1) \cap ((1 \dots j) \cup (j + 1 \dots M)) = ((j + 1 \dots M + 1) \cap (1 \dots j)) \cup ((j + 1 \dots M + 1) \cap (j + 1 \dots M))$
262	260 261	eqtr4i	$⊢ ((j + 1 \dots M + 1) \cap (j + 1 \dots M)) \cup ((j + 1 \dots M + 1) \cap (1 \dots j)) = (j + 1 \dots M + 1) \cap ((1 \dots j) \cup (j + 1 \dots M))$
263		un0	$⊢ (j + 1 \dots M) \cup \emptyset = (j + 1 \dots M)$
264	259 262 263	3eqtr3g	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \cap ((1 \dots j) \cup (j + 1 \dots M)) = (j + 1 \dots M)$
265	252 264	eqtrd	$⊢ j \in (0 \dots M) \to (j + 1 \dots M + 1) \cap (1 \dots M) = (j + 1 \dots M)$
266	265	reseq2d	$⊢ j \in (0 \dots M) \to {U ↾}_{((j + 1 \dots M + 1) \cap (1 \dots M))} = {U ↾}_{(j + 1 \dots M)}$
267	251 266	sylan9req	$⊢ (φ \land j \in (0 \dots M)) \to {U ↾}_{(j + 1 \dots M + 1)} = {U ↾}_{(j + 1 \dots M)}$
268	267	rneqd	$⊢ (φ \land j \in (0 \dots M)) \to ran ({U ↾}_{(j + 1 \dots M + 1)}) = ran ({U ↾}_{(j + 1 \dots M)})$
269		df-ima	$⊢ U [(j + 1 \dots M + 1)] = ran ({U ↾}_{(j + 1 \dots M + 1)})$
270		df-ima	$⊢ U [(j + 1 \dots M)] = ran ({U ↾}_{(j + 1 \dots M)})$
271	268 269 270	3eqtr4g	$⊢ (φ \land j \in (0 \dots M)) \to U [(j + 1 \dots M + 1)] = U [(j + 1 \dots M)]$
272	271	xpeq1d	$⊢ (φ \land j \in (0 \dots M)) \to U [(j + 1 \dots M + 1)] \times \{0\} = U [(j + 1 \dots M)] \times \{0\}$
273	272	reseq1d	$⊢ (φ \land j \in (0 \dots M)) \to {(U [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = {(U [(j + 1 \dots M)] \times \{0\}) ↾}_{(1 \dots M)}$
274		relxp	$⊢ Rel (U [(j + 1 \dots M)] \times \{0\})$
275		dmxpss	$⊢ dom (U [(j + 1 \dots M)] \times \{0\}) \subseteq U [(j + 1 \dots M)]$
276		imassrn	$⊢ U [(j + 1 \dots M)] \subseteq ran U$
277	275 276	sstri	$⊢ dom (U [(j + 1 \dots M)] \times \{0\}) \subseteq ran U$
278	277 216	sstrid	$⊢ φ \to dom (U [(j + 1 \dots M)] \times \{0\}) \subseteq (1 \dots M)$
279		relssres	$⊢ (Rel (U [(j + 1 \dots M)] \times \{0\}) \land dom (U [(j + 1 \dots M)] \times \{0\}) \subseteq (1 \dots M)) \to {(U [(j + 1 \dots M)] \times \{0\}) ↾}_{(1 \dots M)} = U [(j + 1 \dots M)] \times \{0\}$
280	274 278 279	sylancr	$⊢ φ \to {(U [(j + 1 \dots M)] \times \{0\}) ↾}_{(1 \dots M)} = U [(j + 1 \dots M)] \times \{0\}$
281	280	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(U [(j + 1 \dots M)] \times \{0\}) ↾}_{(1 \dots M)} = U [(j + 1 \dots M)] \times \{0\}$
282	273 281	eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to {(U [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = U [(j + 1 \dots M)] \times \{0\}$
283		imassrn	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \subseteq ran \{⟨M + 1, M + 1⟩\}$
284	283 222	sseqtri	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \subseteq \{M + 1\}$
285		ssrin	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \subseteq \{M + 1\} \to \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) \subseteq \{M + 1\} \cap (1 \dots M)$
286	284 285	ax-mp	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) \subseteq \{M + 1\} \cap (1 \dots M)$
287	286 227	sseqtrid	$⊢ φ \to \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) \subseteq \emptyset$
288		ss0	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) \subseteq \emptyset \to \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) = \emptyset$
289	287 288	syl	$⊢ φ \to \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) = \emptyset$
290		fnconstg	$⊢ 0 \in V \to (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) Fn \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]$
291		fnresdisj	$⊢ (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) Fn \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \to (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) = \emptyset \leftrightarrow {(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = \emptyset)$
292	13 290 291	mp2b	$⊢ \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \cap (1 \dots M) = \emptyset \leftrightarrow {(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = \emptyset$
293	289 292	sylib	$⊢ φ \to {(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = \emptyset$
294	293	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = \emptyset$
295	282 294	uneq12d	$⊢ (φ \land j \in (0 \dots M)) \to ({(U [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) = (U [(j + 1 \dots M)] \times \{0\}) \cup \emptyset$
296	173	xpeq1i	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\} = (U [(j + 1 \dots M + 1)] \cup \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]) \times \{0\}$
297		xpundir	$⊢ (U [(j + 1 \dots M + 1)] \cup \{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)]) \times \{0\} = (U [(j + 1 \dots M + 1)] \times \{0\}) \cup (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\})$
298	296 297	eqtri	$⊢ (U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\} = (U [(j + 1 \dots M + 1)] \times \{0\}) \cup (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\})$
299	298	reseq1i	$⊢ {((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = {((U [(j + 1 \dots M + 1)] \times \{0\}) \cup (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)}$
300		resundir	$⊢ {((U [(j + 1 \dots M + 1)] \times \{0\}) \cup (\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)} = ({(U [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)})$
301	299 300	eqtr2i	$⊢ ({(U [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) \cup ({(\{⟨M + 1, M + 1⟩\} [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) = {((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}$
302		un0	$⊢ (U [(j + 1 \dots M)] \times \{0\}) \cup \emptyset = U [(j + 1 \dots M)] \times \{0\}$
303	295 301 302	3eqtr3g	$⊢ (φ \land j \in (0 \dots M)) \to {((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)} = U [(j + 1 \dots M)] \times \{0\}$
304	245 303	uneq12d	$⊢ (φ \land j \in (0 \dots M)) \to ({((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) ↾}_{(1 \dots M)}) \cup ({((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}) ↾}_{(1 \dots M)}) = (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})$
305	209 304	eqtrid	$⊢ (φ \land j \in (0 \dots M)) \to {(((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)} = (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})$
306	305	fveq1d	$⊢ (φ \land j \in (0 \dots M)) \to ({(((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) ↾}_{(1 \dots M)}) (n) = ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)$
307	208 306	sylan9eqr	$⊢ ((φ \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)$
308	206 307	oveq12d	$⊢ ((φ \land j \in (0 \dots M)) \land n \in (1 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n) = T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)$
309	308	mpteq2dva	$⊢ (φ \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n)) = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n))$
310	309	uneq1d	$⊢ (φ \land j \in (0 \dots M)) \to (n \in (1 \dots M) ⟼ (T \cup \{⟨M + 1, 0⟩\}) (n) + (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\} = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}$
311	152 200 310	3eqtr2d	$⊢ (φ \land j \in (0 \dots M)) \to (T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\})) = (n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}$
312	311	uneq1d	$⊢ (φ \land j \in (0 \dots M)) \to ((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\}) = ((n \in (1 \dots M) ⟼ T (n) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\})) (n)) \cup \{⟨M + 1, 0⟩\}) \cup ((M + 1 + 1 \dots N) \times \{0\})$
313	81 312	eqtr4d	$⊢ (φ \land j \in (0 \dots M)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\}) = ((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})$
314	313	csbeq1d	$⊢ (φ \land j \in (0 \dots M)) \to ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B$
315	314	eqeq2d	$⊢ (φ \land j \in (0 \dots M)) \to (i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
316	315	rexbidva	$⊢ φ \to (\exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \leftrightarrow \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
317	316	ralbidv	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(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 = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
318	317	biimpd	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to \forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B)$
319		f1ofn	$⊢ U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to U Fn (1 \dots M)$
320	6 319	syl	$⊢ φ \to U Fn (1 \dots M)$
321	73 73	fnsn	$⊢ \{⟨M + 1, M + 1⟩\} Fn \{M + 1\}$
322		fvun2	$⊢ (U Fn (1 \dots M) \land \{⟨M + 1, M + 1⟩\} Fn \{M + 1\} \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land M + 1 \in \{M + 1\})) \to (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = \{⟨M + 1, M + 1⟩\} (M + 1)$
323	321 322	mp3an2	$⊢ (U Fn (1 \dots M) \land ((1 \dots M) \cap \{M + 1\} = \emptyset \land M + 1 \in \{M + 1\})) \to (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = \{⟨M + 1, M + 1⟩\} (M + 1)$
324	168 323	mpanr2	$⊢ (U Fn (1 \dots M) \land (1 \dots M) \cap \{M + 1\} = \emptyset) \to (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = \{⟨M + 1, M + 1⟩\} (M + 1)$
325	320 91 324	syl2anc	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = \{⟨M + 1, M + 1⟩\} (M + 1)$
326	73 73	fvsn	$⊢ \{⟨M + 1, M + 1⟩\} (M + 1) = M + 1$
327	325 326	eqtrdi	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1$
328	185 327	jca	$⊢ φ \to ((T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1)$
329	318 328	jctird	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land ((T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1)))$
330		3anass	$⊢ (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1) \leftrightarrow (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land ((T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1))$
331	329 330	imbitrrdi	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1))$
332	5 94	jctir	$⊢ φ \to (T : (1 \dots M) ⟶ (0 ..^K) \land \{⟨M + 1, 0⟩\} : \{M + 1\} ⟶ \{0\})$
333	332 91 95	syl2anc	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M) \cup \{M + 1\} ⟶ (0 ..^K) \cup \{0\}$
334	333 112	mpbid	$⊢ φ \to (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M + 1) ⟶ (0 ..^K)$
335		ovex	$⊢ (0 ..^K) \in V$
336		ovex	$⊢ (1 \dots M + 1) \in V$
337	335 336	elmap	$⊢ T \cup \{⟨M + 1, 0⟩\} \in ({(0 ..^K)}^{(1 \dots M + 1)}) \leftrightarrow (T \cup \{⟨M + 1, 0⟩\}) : (1 \dots M + 1) ⟶ (0 ..^K)$
338	334 337	sylibr	$⊢ φ \to T \cup \{⟨M + 1, 0⟩\} \in ({(0 ..^K)}^{(1 \dots M + 1)})$
339		ovex	$⊢ (1 \dots M) \in V$
340		f1oexrnex	$⊢ (U : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \land (1 \dots M) \in V) \to U \in V$
341	6 339 340	sylancl	$⊢ φ \to U \in V$
342		snex	$⊢ \{⟨M + 1, M + 1⟩\} \in V$
343		unexg	$⊢ (U \in V \land \{⟨M + 1, M + 1⟩\} \in V) \to U \cup \{⟨M + 1, M + 1⟩\} \in V$
344	341 342 343	sylancl	$⊢ φ \to U \cup \{⟨M + 1, M + 1⟩\} \in V$
345		f1oeq1	$⊢ f = U \cup \{⟨M + 1, M + 1⟩\} \to (f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1))$
346	345	elabg	$⊢ U \cup \{⟨M + 1, M + 1⟩\} \in V \to (U \cup \{⟨M + 1, M + 1⟩\} \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\} \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1))$
347	344 346	syl	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\} \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\} \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1))$
348		f1oeq23	$⊢ ((1 \dots M + 1) = (1 \dots M) \cup \{M + 1\} \land (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}) \to ((U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\})$
349	105 105 348	syl2anc	$⊢ φ \to ((U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1) \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\})$
350	347 349	bitrd	$⊢ φ \to (U \cup \{⟨M + 1, M + 1⟩\} \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\} \leftrightarrow (U \cup \{⟨M + 1, M + 1⟩\}) : (1 \dots M) \cup \{M + 1\} \underset{1-1 onto}{⟶} (1 \dots M) \cup \{M + 1\})$
351	124 350	mpbird	$⊢ φ \to U \cup \{⟨M + 1, M + 1⟩\} \in \{f \| f : (1 \dots M + 1) \underset{1-1 onto}{⟶} (1 \dots M + 1)\}$
352	338 351	opelxpd	$⊢ φ \to ⟨T \cup \{⟨M + 1, 0⟩\}, U \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)\})$
353	331 352	jctild	$⊢ φ \to (\forall i \in (0 \dots M) \exists j \in (0 \dots M) i = ⦋ ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots M)] \times \{0\}))) \cup ((M + 1 \dots N) \times \{0\})) / p ⦌ B \to (⟨T \cup \{⟨M + 1, 0⟩\}, U \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 = ⦋ (((T \cup \{⟨M + 1, 0⟩\}) +_{f} (((U \cup \{⟨M + 1, M + 1⟩\}) [(1 \dots j)] \times \{1\}) \cup ((U \cup \{⟨M + 1, M + 1⟩\}) [(j + 1 \dots M + 1)] \times \{0\}))) \cup ((M + 1 + 1 \dots N) \times \{0\})) / p ⦌ B \land (T \cup \{⟨M + 1, 0⟩\}) (M + 1) = 0 \land (U \cup \{⟨M + 1, M + 1⟩\}) (M + 1) = M + 1)))$

Metamath Proof Explorer

Theorem poimirlem3

Proof