poimirlem24

Description: Lemma for poimir , two ways of expressing that a simplex has 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 ℕ$
	poimirlem28.1	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to B = C$
	poimirlem28.2	$⊢ (φ \land p : (1 \dots N) ⟶ (0 \dots K)) \to B \in (0 \dots N)$
	poimirlem25.3	$⊢ φ \to T : (1 \dots N) ⟶ (0 ..^K)$
	poimirlem25.4	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
	poimirlem24.5	$⊢ φ \to V \in (0 \dots N)$
Assertion	poimirlem24	$⊢ φ \to (\exists x \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) (x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \land ((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \land \exists p \in ran x p (N) \neq 0)) \leftrightarrow (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \land \neg (V = N \land (T (N) = 0 \land U (N) = N))))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem28.1	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to B = C$
3		poimirlem28.2	$⊢ (φ \land p : (1 \dots N) ⟶ (0 \dots K)) \to B \in (0 \dots N)$
4		poimirlem25.3	$⊢ φ \to T : (1 \dots N) ⟶ (0 ..^K)$
5		poimirlem25.4	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
6		poimirlem24.5	$⊢ φ \to V \in (0 \dots N)$
7		nfv	$⊢ Ⅎ j (φ \land y \in (0 \dots N - 1))$
8		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
9		nfcv	$⊢ \underline{Ⅎ} j (1 \dots N)$
10		nfcv	$⊢ \underline{Ⅎ} j (0 \dots K)$
11	8 9 10	nff	$⊢ Ⅎ j ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
12	7 11	nfim	$⊢ Ⅎ j ((φ \land y \in (0 \dots N - 1)) \to ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
13		eleq1	$⊢ j = y \to (j \in (0 \dots N - 1) \leftrightarrow y \in (0 \dots N - 1))$
14	13	anbi2d	$⊢ j = y \to ((φ \land j \in (0 \dots N - 1)) \leftrightarrow (φ \land y \in (0 \dots N - 1)))$
15		csbeq1a	$⊢ j = y \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
16	15	feq1d	$⊢ j = y \to ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K) \leftrightarrow ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
17	14 16	imbi12d	$⊢ j = y \to (((φ \land j \in (0 \dots N - 1)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)) \leftrightarrow ((φ \land y \in (0 \dots N - 1)) \to ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)))$
18	1	nncnd	$⊢ φ \to N \in ℂ$
19		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
20	18 19	syl	$⊢ φ \to N - 1 + 1 = N$
21	1	nnzd	$⊢ φ \to N \in ℤ$
22		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
23	21 22	syl	$⊢ φ \to N - 1 \in ℤ$
24		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
25		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
26	23 24 25	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
27	20 26	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
28		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 \dots N - 1) \subseteq (0 \dots N)$
29	27 28	syl	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
30	29	sselda	$⊢ (φ \land j \in (0 \dots N - 1)) \to j \in (0 \dots N)$
31		elun	$⊢ y \in (\{1\} \cup \{0\}) \leftrightarrow (y \in \{1\} \lor y \in \{0\})$
32		fzofzp1	$⊢ x \in (0 ..^K) \to x + 1 \in (0 \dots K)$
33		elsni	$⊢ y \in \{1\} \to y = 1$
34	33	oveq2d	$⊢ y \in \{1\} \to x + y = x + 1$
35	34	eleq1d	$⊢ y \in \{1\} \to (x + y \in (0 \dots K) \leftrightarrow x + 1 \in (0 \dots K))$
36	32 35	syl5ibrcom	$⊢ x \in (0 ..^K) \to (y \in \{1\} \to x + y \in (0 \dots K))$
37		elfzoelz	$⊢ x \in (0 ..^K) \to x \in ℤ$
38	37	zcnd	$⊢ x \in (0 ..^K) \to x \in ℂ$
39	38	addid1d	$⊢ x \in (0 ..^K) \to x + 0 = x$
40		elfzofz	$⊢ x \in (0 ..^K) \to x \in (0 \dots K)$
41	39 40	eqeltrd	$⊢ x \in (0 ..^K) \to x + 0 \in (0 \dots K)$
42		elsni	$⊢ y \in \{0\} \to y = 0$
43	42	oveq2d	$⊢ y \in \{0\} \to x + y = x + 0$
44	43	eleq1d	$⊢ y \in \{0\} \to (x + y \in (0 \dots K) \leftrightarrow x + 0 \in (0 \dots K))$
45	41 44	syl5ibrcom	$⊢ x \in (0 ..^K) \to (y \in \{0\} \to x + y \in (0 \dots K))$
46	36 45	jaod	$⊢ x \in (0 ..^K) \to ((y \in \{1\} \lor y \in \{0\}) \to x + y \in (0 \dots K))$
47	31 46	syl5bi	$⊢ x \in (0 ..^K) \to (y \in (\{1\} \cup \{0\}) \to x + y \in (0 \dots K))$
48	47	imp	$⊢ (x \in (0 ..^K) \land y \in (\{1\} \cup \{0\})) \to x + y \in (0 \dots K)$
49	48	adantl	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in (0 ..^K) \land y \in (\{1\} \cup \{0\}))) \to x + y \in (0 \dots K)$
50	4	adantr	$⊢ (φ \land j \in (0 \dots N)) \to T : (1 \dots N) ⟶ (0 ..^K)$
51		1ex	$⊢ 1 \in V$
52	51	fconst	$⊢ (U [(1 \dots j)] \times \{1\}) : U [(1 \dots j)] ⟶ \{1\}$
53		c0ex	$⊢ 0 \in V$
54	53	fconst	$⊢ (U [(j + 1 \dots N)] \times \{0\}) : U [(j + 1 \dots N)] ⟶ \{0\}$
55	52 54	pm3.2i	$⊢ ((U [(1 \dots j)] \times \{1\}) : U [(1 \dots j)] ⟶ \{1\} \land (U [(j + 1 \dots N)] \times \{0\}) : U [(j + 1 \dots N)] ⟶ \{0\})$
56		dff1o3	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun U^{-1})$
57	56	simprbi	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun U^{-1}$
58		imain	$⊢ Fun U^{-1} \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [(1 \dots j)] \cap U [(j + 1 \dots N)]$
59	5 57 58	3syl	$⊢ φ \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [(1 \dots j)] \cap U [(j + 1 \dots N)]$
60		elfznn0	$⊢ j \in (0 \dots N) \to j \in ℕ_{0}$
61	60	nn0red	$⊢ j \in (0 \dots N) \to j \in ℝ$
62	61	ltp1d	$⊢ j \in (0 \dots N) \to j < j + 1$
63		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
64	62 63	syl	$⊢ j \in (0 \dots N) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
65	64	imaeq2d	$⊢ j \in (0 \dots N) \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [\emptyset]$
66		ima0	$⊢ U [\emptyset] = \emptyset$
67	65 66	eqtrdi	$⊢ j \in (0 \dots N) \to U [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
68	59 67	sylan9req	$⊢ (φ \land j \in (0 \dots N)) \to U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset$
69		fun	$⊢ (((U [(1 \dots j)] \times \{1\}) : U [(1 \dots j)] ⟶ \{1\} \land (U [(j + 1 \dots N)] \times \{0\}) : U [(j + 1 \dots N)] ⟶ \{0\}) \land U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) : U [(1 \dots j)] \cup U [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
70	55 68 69	sylancr	$⊢ (φ \land j \in (0 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) : U [(1 \dots j)] \cup U [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
71		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
72	60 71	syl	$⊢ j \in (0 \dots N) \to j + 1 \in ℕ$
73		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
74	72 73	eleqtrdi	$⊢ j \in (0 \dots N) \to j + 1 \in ℤ_{\geq 1}$
75		elfzuz3	$⊢ j \in (0 \dots N) \to N \in ℤ_{\geq j}$
76		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq j}) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
77	74 75 76	syl2anc	$⊢ j \in (0 \dots N) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
78	77	imaeq2d	$⊢ j \in (0 \dots N) \to U [(1 \dots N)] = U [(1 \dots j) \cup (j + 1 \dots N)]$
79		imaundi	$⊢ U [(1 \dots j) \cup (j + 1 \dots N)] = U [(1 \dots j)] \cup U [(j + 1 \dots N)]$
80	78 79	eqtr2di	$⊢ j \in (0 \dots N) \to U [(1 \dots j)] \cup U [(j + 1 \dots N)] = U [(1 \dots N)]$
81		f1ofo	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
82		foima	$⊢ U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to U [(1 \dots N)] = (1 \dots N)$
83	5 81 82	3syl	$⊢ φ \to U [(1 \dots N)] = (1 \dots N)$
84	80 83	sylan9eqr	$⊢ (φ \land j \in (0 \dots N)) \to U [(1 \dots j)] \cup U [(j + 1 \dots N)] = (1 \dots N)$
85	84	feq2d	$⊢ (φ \land j \in (0 \dots N)) \to (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) : U [(1 \dots j)] \cup U [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\} \leftrightarrow ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\})$
86	70 85	mpbid	$⊢ (φ \land j \in (0 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
87		ovex	$⊢ (1 \dots N) \in V$
88	87	a1i	$⊢ (φ \land j \in (0 \dots N)) \to (1 \dots N) \in V$
89		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
90	49 50 86 88 88 89	off	$⊢ (φ \land j \in (0 \dots N)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
91	30 90	syldan	$⊢ (φ \land j \in (0 \dots N - 1)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
92	12 17 91	chvarfv	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
93		fzp1elp1	$⊢ y \in (0 \dots N - 1) \to y + 1 \in (0 \dots N - 1 + 1)$
94	20	oveq2d	$⊢ φ \to (0 \dots N - 1 + 1) = (0 \dots N)$
95	94	eleq2d	$⊢ φ \to (y + 1 \in (0 \dots N - 1 + 1) \leftrightarrow y + 1 \in (0 \dots N))$
96	95	biimpa	$⊢ (φ \land y + 1 \in (0 \dots N - 1 + 1)) \to y + 1 \in (0 \dots N)$
97	93 96	sylan2	$⊢ (φ \land y \in (0 \dots N - 1)) \to y + 1 \in (0 \dots N)$
98		nfv	$⊢ Ⅎ j (φ \land y + 1 \in (0 \dots N))$
99		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
100	99 9 10	nff	$⊢ Ⅎ j ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
101	98 100	nfim	$⊢ Ⅎ j ((φ \land y + 1 \in (0 \dots N)) \to ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
102		ovex	$⊢ y + 1 \in V$
103		eleq1	$⊢ j = y + 1 \to (j \in (0 \dots N) \leftrightarrow y + 1 \in (0 \dots N))$
104	103	anbi2d	$⊢ j = y + 1 \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land y + 1 \in (0 \dots N)))$
105		csbeq1a	$⊢ j = y + 1 \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
106	105	feq1d	$⊢ j = y + 1 \to ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K) \leftrightarrow ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
107	104 106	imbi12d	$⊢ j = y + 1 \to (((φ \land j \in (0 \dots N)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)) \leftrightarrow ((φ \land y + 1 \in (0 \dots N)) \to ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)))$
108	101 102 107 90	vtoclf	$⊢ (φ \land y + 1 \in (0 \dots N)) \to ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
109	97 108	syldan	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
110		csbeq1	$⊢ y = if (y < V, y, y + 1) \to ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
111	110	feq1d	$⊢ y = if (y < V, y, y + 1) \to (⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K) \leftrightarrow ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
112		csbeq1	$⊢ y + 1 = if (y < V, y, y + 1) \to ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
113	112	feq1d	$⊢ y + 1 = if (y < V, y, y + 1) \to (⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K) \leftrightarrow ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
114	111 113	ifboth	$⊢ (⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K) \land ⦋ (y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)) \to ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
115	92 109 114	syl2anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
116		ovex	$⊢ (0 \dots K) \in V$
117	116 87	elmap	$⊢ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \in ({(0 \dots K)}^{(1 \dots N)}) \leftrightarrow ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
118	115 117	sylibr	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \in ({(0 \dots K)}^{(1 \dots N)})$
119	118	fmpttd	$⊢ φ \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
120		ovex	$⊢ {(0 \dots K)}^{(1 \dots N)} \in V$
121		ovex	$⊢ (0 \dots N - 1) \in V$
122	120 121	elmap	$⊢ (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) \leftrightarrow (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
123	119 122	sylibr	$⊢ φ \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)})$
124		rneq	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to ran x = ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))))$
125	124	mpteq1d	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to (p \in ran x ⟼ B) = (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B)$
126	125	rneqd	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to ran (p \in ran x ⟼ B) = ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B)$
127	126	sseq2d	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to ((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \leftrightarrow (0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B))$
128	124	rexeqdv	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to (\exists p \in ran x p (N) \neq 0 \leftrightarrow \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0)$
129	127 128	anbi12d	$⊢ x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \to (((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \land \exists p \in ran x p (N) \neq 0) \leftrightarrow ((0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0))$
130	129	ceqsrexv	$⊢ (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) \to (\exists x \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) (x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \land ((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \land \exists p \in ran x p (N) \neq 0)) \leftrightarrow ((0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0))$
131	123 130	syl	$⊢ φ \to (\exists x \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) (x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \land ((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \land \exists p \in ran x p (N) \neq 0)) \leftrightarrow ((0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0))$
132		dfss3	$⊢ (0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \forall i \in (0 \dots N - 1) i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B)$
133		ovex	$⊢ 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \in V$
134	133 2	csbie	$⊢ ⦋ (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = C$
135	134	csbeq2i	$⊢ ⦋ ⟨T, U⟩ / s ⦌ ⦋ (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = ⦋ ⟨T, U⟩ / s ⦌ C$
136		opex	$⊢ ⟨T, U⟩ \in V$
137	136	a1i	$⊢ φ \to ⟨T, U⟩ \in V$
138		fveq2	$⊢ s = ⟨T, U⟩ \to 1^{st} (s) = 1^{st} (⟨T, U⟩)$
139		fex	$⊢ (T : (1 \dots N) ⟶ (0 ..^K) \land (1 \dots N) \in V) \to T \in V$
140	4 87 139	sylancl	$⊢ φ \to T \in V$
141		f1oexrnex	$⊢ (U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land (1 \dots N) \in V) \to U \in V$
142	5 87 141	sylancl	$⊢ φ \to U \in V$
143		op1stg	$⊢ (T \in V \land U \in V) \to 1^{st} (⟨T, U⟩) = T$
144	140 142 143	syl2anc	$⊢ φ \to 1^{st} (⟨T, U⟩) = T$
145	138 144	sylan9eqr	$⊢ (φ \land s = ⟨T, U⟩) \to 1^{st} (s) = T$
146		fveq2	$⊢ s = ⟨T, U⟩ \to 2^{nd} (s) = 2^{nd} (⟨T, U⟩)$
147		op2ndg	$⊢ (T \in V \land U \in V) \to 2^{nd} (⟨T, U⟩) = U$
148	140 142 147	syl2anc	$⊢ φ \to 2^{nd} (⟨T, U⟩) = U$
149	146 148	sylan9eqr	$⊢ (φ \land s = ⟨T, U⟩) \to 2^{nd} (s) = U$
150		imaeq1	$⊢ 2^{nd} (s) = U \to 2^{nd} (s) [(1 \dots j)] = U [(1 \dots j)]$
151	150	xpeq1d	$⊢ 2^{nd} (s) = U \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = U [(1 \dots j)] \times \{1\}$
152		imaeq1	$⊢ 2^{nd} (s) = U \to 2^{nd} (s) [(j + 1 \dots N)] = U [(j + 1 \dots N)]$
153	152	xpeq1d	$⊢ 2^{nd} (s) = U \to 2^{nd} (s) [(j + 1 \dots N)] \times \{0\} = U [(j + 1 \dots N)] \times \{0\}$
154	151 153	uneq12d	$⊢ 2^{nd} (s) = U \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})$
155	149 154	syl	$⊢ (φ \land s = ⟨T, U⟩) \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})$
156	145 155	oveq12d	$⊢ (φ \land s = ⟨T, U⟩) \to 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))$
157	156	csbeq1d	$⊢ (φ \land s = ⟨T, U⟩) \to ⦋ (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
158	137 157	csbied	$⊢ φ \to ⦋ ⟨T, U⟩ / s ⦌ ⦋ (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
159	135 158	eqtr3id	$⊢ φ \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
160	159	csbeq2dv	$⊢ φ \to ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
161	160	eqeq2d	$⊢ φ \to (i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B)$
162	161	rexbidv	$⊢ φ \to (\exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B)$
163		vex	$⊢ i \in V$
164		eqid	$⊢ (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) = (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B)$
165	164	elrnmpt	$⊢ i \in V \to (i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = B)$
166	163 165	ax-mp	$⊢ i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = B$
167		nfv	$⊢ Ⅎ k i = B$
168		nfcsb1v	$⊢ \underline{Ⅎ} p ⦋ k / p ⦌ B$
169	168	nfeq2	$⊢ Ⅎ p i = ⦋ k / p ⦌ B$
170		csbeq1a	$⊢ p = k \to B = ⦋ k / p ⦌ B$
171	170	eqeq2d	$⊢ p = k \to (i = B \leftrightarrow i = ⦋ k / p ⦌ B)$
172	167 169 171	cbvrexw	$⊢ \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = B \leftrightarrow \exists k \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = ⦋ k / p ⦌ B$
173		ovex	$⊢ T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) \in V$
174	173	csbex	$⊢ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \in V$
175	174	rgenw	$⊢ \forall y \in (0 \dots N - 1) ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \in V$
176		eqid	$⊢ (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))))$
177		csbeq1	$⊢ k = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \to ⦋ k / p ⦌ B = ⦋ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
178		vex	$⊢ y \in V$
179	178 102	ifex	$⊢ if (y < V, y, y + 1) \in V$
180		csbnestgw	$⊢ if (y < V, y, y + 1) \in V \to ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = ⦋ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
181	179 180	ax-mp	$⊢ ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B = ⦋ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
182	177 181	eqtr4di	$⊢ k = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \to ⦋ k / p ⦌ B = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
183	182	eqeq2d	$⊢ k = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \to (i = ⦋ k / p ⦌ B \leftrightarrow i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B)$
184	176 183	rexrnmptw	$⊢ \forall y \in (0 \dots N - 1) ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) \in V \to (\exists k \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = ⦋ k / p ⦌ B \leftrightarrow \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B)$
185	175 184	ax-mp	$⊢ \exists k \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) i = ⦋ k / p ⦌ B \leftrightarrow \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
186	166 172 185	3bitri	$⊢ i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) / p ⦌ B$
187	162 186	bitr4di	$⊢ φ \to (\exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B))$
188	29	sselda	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \in (0 \dots N)$
189	188	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < V) \to y \in (0 \dots N)$
190		elfzelz	$⊢ y \in (0 \dots N - 1) \to y \in ℤ$
191	190	zred	$⊢ y \in (0 \dots N - 1) \to y \in ℝ$
192	191	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \in ℝ$
193		ltne	$⊢ (y \in ℝ \land y < V) \to V \neq y$
194	193	necomd	$⊢ (y \in ℝ \land y < V) \to y \neq V$
195	192 194	sylan	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < V) \to y \neq V$
196		eldifsn	$⊢ y \in ((0 \dots N) ∖ \{V\}) \leftrightarrow (y \in (0 \dots N) \land y \neq V)$
197	189 195 196	sylanbrc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land y < V) \to y \in ((0 \dots N) ∖ \{V\})$
198	97	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < V) \to y + 1 \in (0 \dots N)$
199	6	elfzelzd	$⊢ φ \to V \in ℤ$
200	199	zred	$⊢ φ \to V \in ℝ$
201	200	ad2antrr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < V) \to V \in ℝ$
202		zre	$⊢ V \in ℤ \to V \in ℝ$
203		zre	$⊢ y \in ℤ \to y \in ℝ$
204		lenlt	$⊢ (V \in ℝ \land y \in ℝ) \to (V \leq y \leftrightarrow \neg y < V)$
205	202 203 204	syl2an	$⊢ (V \in ℤ \land y \in ℤ) \to (V \leq y \leftrightarrow \neg y < V)$
206		zleltp1	$⊢ (V \in ℤ \land y \in ℤ) \to (V \leq y \leftrightarrow V < y + 1)$
207	205 206	bitr3d	$⊢ (V \in ℤ \land y \in ℤ) \to (\neg y < V \leftrightarrow V < y + 1)$
208	199 190 207	syl2an	$⊢ (φ \land y \in (0 \dots N - 1)) \to (\neg y < V \leftrightarrow V < y + 1)$
209	208	biimpa	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < V) \to V < y + 1$
210	201 209	gtned	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < V) \to y + 1 \neq V$
211		eldifsn	$⊢ y + 1 \in ((0 \dots N) ∖ \{V\}) \leftrightarrow (y + 1 \in (0 \dots N) \land y + 1 \neq V)$
212	198 210 211	sylanbrc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land \neg y < V) \to y + 1 \in ((0 \dots N) ∖ \{V\})$
213	197 212	ifclda	$⊢ (φ \land y \in (0 \dots N - 1)) \to if (y < V, y, y + 1) \in ((0 \dots N) ∖ \{V\})$
214		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
215	214	nfeq2	$⊢ Ⅎ j i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
216		csbeq1a	$⊢ j = if (y < V, y, y + 1) \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
217	216	eqeq2d	$⊢ j = if (y < V, y, y + 1) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
218	215 217	rspce	$⊢ (if (y < V, y, y + 1) \in ((0 \dots N) ∖ \{V\}) \land i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
219	218	ex	$⊢ if (y < V, y, y + 1) \in ((0 \dots N) ∖ \{V\}) \to (i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
220	213 219	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
221	220	rexlimdva	$⊢ φ \to (\exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
222		nfv	$⊢ Ⅎ j φ$
223		nfcv	$⊢ \underline{Ⅎ} j (0 \dots N - 1)$
224	223 215	nfrex	$⊢ Ⅎ j \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
225		eldifi	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \in (0 \dots N)$
226	225 60	syl	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \in ℕ_{0}$
227	226	nn0ge0d	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to 0 \leq j$
228	227	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to 0 \leq j$
229	226	nn0red	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \in ℝ$
230	229	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j \in ℝ$
231	200	ad2antrr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to V \in ℝ$
232	21	zred	$⊢ φ \to N \in ℝ$
233	232	ad2antrr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to N \in ℝ$
234		simpr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j < V$
235		elfzle2	$⊢ V \in (0 \dots N) \to V \leq N$
236	6 235	syl	$⊢ φ \to V \leq N$
237	236	ad2antrr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to V \leq N$
238	230 231 233 234 237	ltletrd	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j < N$
239	225	elfzelzd	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \in ℤ$
240		zltlem1	$⊢ (j \in ℤ \land N \in ℤ) \to (j < N \leftrightarrow j \leq N - 1)$
241	239 21 240	syl2anr	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j < N \leftrightarrow j \leq N - 1)$
242	241	adantr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to (j < N \leftrightarrow j \leq N - 1)$
243	238 242	mpbid	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j \leq N - 1$
244		0z	$⊢ 0 \in ℤ$
245		elfz	$⊢ (j \in ℤ \land 0 \in ℤ \land N - 1 \in ℤ) \to (j \in (0 \dots N - 1) \leftrightarrow (0 \leq j \land j \leq N - 1))$
246	244 245	mp3an2	$⊢ (j \in ℤ \land N - 1 \in ℤ) \to (j \in (0 \dots N - 1) \leftrightarrow (0 \leq j \land j \leq N - 1))$
247	239 23 246	syl2anr	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j \in (0 \dots N - 1) \leftrightarrow (0 \leq j \land j \leq N - 1))$
248	247	adantr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to (j \in (0 \dots N - 1) \leftrightarrow (0 \leq j \land j \leq N - 1))$
249	228 243 248	mpbir2and	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j \in (0 \dots N - 1)$
250		0red	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to 0 \in ℝ$
251	200	ad2antrr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to V \in ℝ$
252	229	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j \in ℝ$
253		elfzle1	$⊢ V \in (0 \dots N) \to 0 \leq V$
254	6 253	syl	$⊢ φ \to 0 \leq V$
255	254	ad2antrr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to 0 \leq V$
256		lenlt	$⊢ (V \in ℝ \land j \in ℝ) \to (V \leq j \leftrightarrow \neg j < V)$
257	200 229 256	syl2an	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (V \leq j \leftrightarrow \neg j < V)$
258	257	biimpar	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to V \leq j$
259		eldifsni	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \neq V$
260	259	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j \neq V$
261		ltlen	$⊢ (V \in ℝ \land j \in ℝ) \to (V < j \leftrightarrow (V \leq j \land j \neq V))$
262	200 229 261	syl2an	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (V < j \leftrightarrow (V \leq j \land j \neq V))$
263	262	adantr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to (V < j \leftrightarrow (V \leq j \land j \neq V))$
264	258 260 263	mpbir2and	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to V < j$
265	250 251 252 255 264	lelttrd	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to 0 < j$
266		zgt0ge1	$⊢ j \in ℤ \to (0 < j \leftrightarrow 1 \leq j)$
267	239 266	syl	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to (0 < j \leftrightarrow 1 \leq j)$
268	267	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to (0 < j \leftrightarrow 1 \leq j)$
269	265 268	mpbid	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to 1 \leq j$
270		elfzle2	$⊢ j \in (0 \dots N) \to j \leq N$
271	225 270	syl	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \leq N$
272	271	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j \leq N$
273		1z	$⊢ 1 \in ℤ$
274		elfz	$⊢ (j \in ℤ \land 1 \in ℤ \land N \in ℤ) \to (j \in (1 \dots N) \leftrightarrow (1 \leq j \land j \leq N))$
275	273 274	mp3an2	$⊢ (j \in ℤ \land N \in ℤ) \to (j \in (1 \dots N) \leftrightarrow (1 \leq j \land j \leq N))$
276	239 21 275	syl2anr	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j \in (1 \dots N) \leftrightarrow (1 \leq j \land j \leq N))$
277	276	adantr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to (j \in (1 \dots N) \leftrightarrow (1 \leq j \land j \leq N))$
278	269 272 277	mpbir2and	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j \in (1 \dots N)$
279		elfzmlbm	$⊢ j \in (1 \dots N) \to j - 1 \in (0 \dots N - 1)$
280	278 279	syl	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j - 1 \in (0 \dots N - 1)$
281	249 280	ifclda	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to if (j < V, j, j - 1) \in (0 \dots N - 1)$
282		breq1	$⊢ j = if (j < V, j, j - 1) \to (j < V \leftrightarrow if (j < V, j, j - 1) < V)$
283		id	$⊢ j = if (j < V, j, j - 1) \to j = if (j < V, j, j - 1)$
284		oveq1	$⊢ j = if (j < V, j, j - 1) \to j + 1 = if (j < V, j, j - 1) + 1$
285	282 283 284	ifbieq12d	$⊢ j = if (j < V, j, j - 1) \to if (j < V, j, j + 1) = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1)$
286	285	eqeq2d	$⊢ j = if (j < V, j, j - 1) \to (j = if (j < V, j, j + 1) \leftrightarrow j = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1))$
287		breq1	$⊢ j - 1 = if (j < V, j, j - 1) \to (j - 1 < V \leftrightarrow if (j < V, j, j - 1) < V)$
288		id	$⊢ j - 1 = if (j < V, j, j - 1) \to j - 1 = if (j < V, j, j - 1)$
289		oveq1	$⊢ j - 1 = if (j < V, j, j - 1) \to j - 1 + 1 = if (j < V, j, j - 1) + 1$
290	287 288 289	ifbieq12d	$⊢ j - 1 = if (j < V, j, j - 1) \to if (j - 1 < V, j - 1, j - 1 + 1) = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1)$
291	290	eqeq2d	$⊢ j - 1 = if (j < V, j, j - 1) \to (j = if (j - 1 < V, j - 1, j - 1 + 1) \leftrightarrow j = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1))$
292		iftrue	$⊢ j < V \to if (j < V, j, j + 1) = j$
293	292	eqcomd	$⊢ j < V \to j = if (j < V, j, j + 1)$
294	293	adantl	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land j < V) \to j = if (j < V, j, j + 1)$
295		zlem1lt	$⊢ (j \in ℤ \land V \in ℤ) \to (j \leq V \leftrightarrow j - 1 < V)$
296	239 199 295	syl2anr	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j \leq V \leftrightarrow j - 1 < V)$
297	259	necomd	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to V \neq j$
298	297	adantl	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to V \neq j$
299		ltlen	$⊢ (j \in ℝ \land V \in ℝ) \to (j < V \leftrightarrow (j \leq V \land V \neq j))$
300	229 200 299	syl2anr	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j < V \leftrightarrow (j \leq V \land V \neq j))$
301	300	biimprd	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to ((j \leq V \land V \neq j) \to j < V)$
302	298 301	mpan2d	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j \leq V \to j < V)$
303	296 302	sylbird	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (j - 1 < V \to j < V)$
304	303	con3dimp	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to \neg j - 1 < V$
305	304	iffalsed	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to if (j - 1 < V, j - 1, j - 1 + 1) = j - 1 + 1$
306	226	nn0cnd	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j \in ℂ$
307		npcan1	$⊢ j \in ℂ \to j - 1 + 1 = j$
308	306 307	syl	$⊢ j \in ((0 \dots N) ∖ \{V\}) \to j - 1 + 1 = j$
309	308	ad2antlr	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j - 1 + 1 = j$
310	305 309	eqtr2d	$⊢ ((φ \land j \in ((0 \dots N) ∖ \{V\})) \land \neg j < V) \to j = if (j - 1 < V, j - 1, j - 1 + 1)$
311	286 291 294 310	ifbothda	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to j = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1)$
312		csbeq1a	$⊢ j = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
313	311 312	syl	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
314	313	eqeq2d	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
315	314	biimpd	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \to i = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
316		breq1	$⊢ y = if (j < V, j, j - 1) \to (y < V \leftrightarrow if (j < V, j, j - 1) < V)$
317		id	$⊢ y = if (j < V, j, j - 1) \to y = if (j < V, j, j - 1)$
318		oveq1	$⊢ y = if (j < V, j, j - 1) \to y + 1 = if (j < V, j, j - 1) + 1$
319	316 317 318	ifbieq12d	$⊢ y = if (j < V, j, j - 1) \to if (y < V, y, y + 1) = if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1)$
320	319	csbeq1d	$⊢ y = if (j < V, j, j - 1) \to ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
321	320	eqeq2d	$⊢ y = if (j < V, j, j - 1) \to (i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
322	321	rspcev	$⊢ (if (j < V, j, j - 1) \in (0 \dots N - 1) \land i = ⦋ if (if (j < V, j, j - 1) < V, if (j < V, j, j - 1), if (j < V, j, j - 1) + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
323	281 315 322	syl6an	$⊢ (φ \land j \in ((0 \dots N) ∖ \{V\})) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
324	323	ex	$⊢ φ \to (j \in ((0 \dots N) ∖ \{V\}) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C))$
325	222 224 324	rexlimd	$⊢ φ \to (\exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
326	221 325	impbid	$⊢ φ \to (\exists y \in (0 \dots N - 1) i = ⦋ if (y < V, y, y + 1) / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
327	187 326	bitr3d	$⊢ φ \to (i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
328	327	ralbidv	$⊢ φ \to (\forall i \in (0 \dots N - 1) i \in ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
329	132 328	syl5bb	$⊢ φ \to ((0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
330	329	anbi1d	$⊢ φ \to (((0 \dots N - 1) \subseteq ran (p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) ⟼ B) \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0) \leftrightarrow (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0))$
331	1 4 5 6	poimirlem23	$⊢ φ \to (\exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0 \leftrightarrow \neg (V = N \land (T (N) = 0 \land U (N) = N)))$
332	331	anbi2d	$⊢ φ \to ((\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \land \exists p \in ran (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) p (N) \neq 0) \leftrightarrow (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \land \neg (V = N \land (T (N) = 0 \land U (N) = N))))$
333	131 330 332	3bitrd	$⊢ φ \to (\exists x \in ({({(0 \dots K)}^{(1 \dots N)})}^{(0 \dots N - 1)}) (x = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))) \land ((0 \dots N - 1) \subseteq ran (p \in ran x ⟼ B) \land \exists p \in ran x p (N) \neq 0)) \leftrightarrow (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{V\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \land \neg (V = N \land (T (N) = 0 \land U (N) = N))))$

Metamath Proof Explorer

Theorem poimirlem24

Proof