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