poimirlem23

Description: Lemma for poimir , two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem23.1	$⊢ φ \to T : (1 \dots N) ⟶ (0 ..^K)$
	poimirlem23.2	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
	poimirlem23.3	$⊢ φ \to V \in (0 \dots N)$
Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem23.1	$⊢ φ \to T : (1 \dots N) ⟶ (0 ..^K)$
3		poimirlem23.2	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
4		poimirlem23.3	$⊢ φ \to V \in (0 \dots N)$
5		ovex	$⊢ T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) \in V$
6	5	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$
7	6	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$
8		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\}))))$
9		fveq1	$⊢ p = ⦋ 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 (N) = ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N)$
10	9	neeq1d	$⊢ p = ⦋ 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 (N) \neq 0 \leftrightarrow ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0)$
11		df-ne	$⊢ ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0 \leftrightarrow \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
12	10 11	bitrdi	$⊢ p = ⦋ 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 (N) \neq 0 \leftrightarrow \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
13	8 12	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 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 \exists y \in (0 \dots N - 1) \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
14	7 13	ax-mp	$⊢ \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 \exists y \in (0 \dots N - 1) \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
15		rexnal	$⊢ \exists y \in (0 \dots N - 1) \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow \neg \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\}))) (N) = 0$
16	14 15	bitri	$⊢ \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 \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\}))) (N) = 0$
17	1	nnzd	$⊢ φ \to N \in ℤ$
18		elfzelz	$⊢ V \in (0 \dots N) \to V \in ℤ$
19	4 18	syl	$⊢ φ \to V \in ℤ$
20		zlem1lt	$⊢ (N \in ℤ \land V \in ℤ) \to (N \leq V \leftrightarrow N - 1 < V)$
21	17 19 20	syl2anc	$⊢ φ \to (N \leq V \leftrightarrow N - 1 < V)$
22		elfzle2	$⊢ V \in (0 \dots N) \to V \leq N$
23	4 22	syl	$⊢ φ \to V \leq N$
24	19	zred	$⊢ φ \to V \in ℝ$
25	1	nnred	$⊢ φ \to N \in ℝ$
26	24 25	letri3d	$⊢ φ \to (V = N \leftrightarrow (V \leq N \land N \leq V))$
27	26	biimprd	$⊢ φ \to ((V \leq N \land N \leq V) \to V = N)$
28	23 27	mpand	$⊢ φ \to (N \leq V \to V = N)$
29	21 28	sylbird	$⊢ φ \to (N - 1 < V \to V = N)$
30	29	necon3ad	$⊢ φ \to (V \neq N \to \neg N - 1 < V)$
31		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
32	1 31	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
33		nn0fz0	$⊢ N - 1 \in ℕ_{0} \leftrightarrow N - 1 \in (0 \dots N - 1)$
34	32 33	sylib	$⊢ φ \to N - 1 \in (0 \dots N - 1)$
35	34	adantr	$⊢ (φ \land \neg N - 1 < V) \to N - 1 \in (0 \dots N - 1)$
36		iffalse	$⊢ \neg N - 1 < V \to if (N - 1 < V, N - 1, N - 1 + 1) = N - 1 + 1$
37	1	nncnd	$⊢ φ \to N \in ℂ$
38		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
39	37 38	syl	$⊢ φ \to N - 1 + 1 = N$
40	36 39	sylan9eqr	$⊢ (φ \land \neg N - 1 < V) \to if (N - 1 < V, N - 1, N - 1 + 1) = N$
41	40	csbeq1d	$⊢ (φ \land \neg N - 1 < V) \to ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = ⦋ N / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
42		oveq2	$⊢ j = N \to (1 \dots j) = (1 \dots N)$
43	42	imaeq2d	$⊢ j = N \to U [(1 \dots j)] = U [(1 \dots N)]$
44	43	xpeq1d	$⊢ j = N \to U [(1 \dots j)] \times \{1\} = U [(1 \dots N)] \times \{1\}$
45		oveq1	$⊢ j = N \to j + 1 = N + 1$
46	45	oveq1d	$⊢ j = N \to (j + 1 \dots N) = (N + 1 \dots N)$
47	46	imaeq2d	$⊢ j = N \to U [(j + 1 \dots N)] = U [(N + 1 \dots N)]$
48	47	xpeq1d	$⊢ j = N \to U [(j + 1 \dots N)] \times \{0\} = U [(N + 1 \dots N)] \times \{0\}$
49	44 48	uneq12d	$⊢ j = N \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots N)] \times \{1\}) \cup (U [(N + 1 \dots N)] \times \{0\})$
50		f1ofo	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
51		foima	$⊢ U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to U [(1 \dots N)] = (1 \dots N)$
52	3 50 51	3syl	$⊢ φ \to U [(1 \dots N)] = (1 \dots N)$
53	52	xpeq1d	$⊢ φ \to U [(1 \dots N)] \times \{1\} = (1 \dots N) \times \{1\}$
54	25	ltp1d	$⊢ φ \to N < N + 1$
55	17	peano2zd	$⊢ φ \to N + 1 \in ℤ$
56		fzn	$⊢ (N + 1 \in ℤ \land N \in ℤ) \to (N < N + 1 \leftrightarrow (N + 1 \dots N) = \emptyset)$
57	55 17 56	syl2anc	$⊢ φ \to (N < N + 1 \leftrightarrow (N + 1 \dots N) = \emptyset)$
58	54 57	mpbid	$⊢ φ \to (N + 1 \dots N) = \emptyset$
59	58	imaeq2d	$⊢ φ \to U [(N + 1 \dots N)] = U [\emptyset]$
60	59	xpeq1d	$⊢ φ \to U [(N + 1 \dots N)] \times \{0\} = U [\emptyset] \times \{0\}$
61		ima0	$⊢ U [\emptyset] = \emptyset$
62	61	xpeq1i	$⊢ U [\emptyset] \times \{0\} = \emptyset \times \{0\}$
63		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
64	62 63	eqtri	$⊢ U [\emptyset] \times \{0\} = \emptyset$
65	60 64	eqtrdi	$⊢ φ \to U [(N + 1 \dots N)] \times \{0\} = \emptyset$
66	53 65	uneq12d	$⊢ φ \to (U [(1 \dots N)] \times \{1\}) \cup (U [(N + 1 \dots N)] \times \{0\}) = ((1 \dots N) \times \{1\}) \cup \emptyset$
67		un0	$⊢ ((1 \dots N) \times \{1\}) \cup \emptyset = (1 \dots N) \times \{1\}$
68	66 67	eqtrdi	$⊢ φ \to (U [(1 \dots N)] \times \{1\}) \cup (U [(N + 1 \dots N)] \times \{0\}) = (1 \dots N) \times \{1\}$
69	49 68	sylan9eqr	$⊢ (φ \land j = N) \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (1 \dots N) \times \{1\}$
70	69	oveq2d	$⊢ (φ \land j = N) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((1 \dots N) \times \{1\})$
71	1 70	csbied	$⊢ φ \to ⦋ N / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((1 \dots N) \times \{1\})$
72	71	adantr	$⊢ (φ \land \neg N - 1 < V) \to ⦋ N / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((1 \dots N) \times \{1\})$
73	41 72	eqtrd	$⊢ (φ \land \neg N - 1 < V) \to ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((1 \dots N) \times \{1\})$
74	73	fveq1d	$⊢ (φ \land \neg N - 1 < V) \to ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = (T +_{f} ((1 \dots N) \times \{1\})) (N)$
75		elfzonn0	$⊢ j \in (0 ..^K) \to j \in ℕ_{0}$
76		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
77	75 76	syl	$⊢ j \in (0 ..^K) \to j + 1 \in ℕ$
78		elsni	$⊢ y \in \{1\} \to y = 1$
79	78	oveq2d	$⊢ y \in \{1\} \to j + y = j + 1$
80	79	eleq1d	$⊢ y \in \{1\} \to (j + y \in ℕ \leftrightarrow j + 1 \in ℕ)$
81	77 80	syl5ibrcom	$⊢ j \in (0 ..^K) \to (y \in \{1\} \to j + y \in ℕ)$
82	81	imp	$⊢ (j \in (0 ..^K) \land y \in \{1\}) \to j + y \in ℕ$
83	82	adantl	$⊢ (φ \land (j \in (0 ..^K) \land y \in \{1\})) \to j + y \in ℕ$
84		1ex	$⊢ 1 \in V$
85	84	fconst	$⊢ ((1 \dots N) \times \{1\}) : (1 \dots N) ⟶ \{1\}$
86	85	a1i	$⊢ φ \to ((1 \dots N) \times \{1\}) : (1 \dots N) ⟶ \{1\}$
87		ovexd	$⊢ φ \to (1 \dots N) \in V$
88		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
89	83 2 86 87 87 88	off	$⊢ φ \to (T +_{f} ((1 \dots N) \times \{1\})) : (1 \dots N) ⟶ ℕ$
90		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
91	1 90	sylib	$⊢ φ \to N \in (1 \dots N)$
92	89 91	ffvelcdmd	$⊢ φ \to (T +_{f} ((1 \dots N) \times \{1\})) (N) \in ℕ$
93	92	adantr	$⊢ (φ \land \neg N - 1 < V) \to (T +_{f} ((1 \dots N) \times \{1\})) (N) \in ℕ$
94	74 93	eqeltrd	$⊢ (φ \land \neg N - 1 < V) \to ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \in ℕ$
95	94	nnne0d	$⊢ (φ \land \neg N - 1 < V) \to ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0$
96		breq1	$⊢ y = N - 1 \to (y < V \leftrightarrow N - 1 < V)$
97		id	$⊢ y = N - 1 \to y = N - 1$
98		oveq1	$⊢ y = N - 1 \to y + 1 = N - 1 + 1$
99	96 97 98	ifbieq12d	$⊢ y = N - 1 \to if (y < V, y, y + 1) = if (N - 1 < V, N - 1, N - 1 + 1)$
100	99	csbeq1d	$⊢ y = 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\}))) = ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
101	100	fveq1d	$⊢ y = 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\}))) (N) = ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N)$
102	101	neeq1d	$⊢ y = 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\}))) (N) \neq 0 \leftrightarrow ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0)$
103	11 102	bitr3id	$⊢ y = N - 1 \to (\neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0)$
104	103	rspcev	$⊢ (N - 1 \in (0 \dots N - 1) \land ⦋ if (N - 1 < V, N - 1, N - 1 + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) \neq 0) \to \exists y \in (0 \dots N - 1) \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
105	35 95 104	syl2anc	$⊢ (φ \land \neg N - 1 < V) \to \exists y \in (0 \dots N - 1) \neg ⦋ if (y < V, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
106	105 15	sylib	$⊢ (φ \land \neg N - 1 < V) \to \neg \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\}))) (N) = 0$
107	106	ex	$⊢ φ \to (\neg N - 1 < V \to \neg \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\}))) (N) = 0)$
108	30 107	syld	$⊢ φ \to (V \neq N \to \neg \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\}))) (N) = 0)$
109	108	necon4ad	$⊢ φ \to (\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\}))) (N) = 0 \to V = N)$
110	109	pm4.71rd	$⊢ φ \to (\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\}))) (N) = 0 \leftrightarrow (V = N \land \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\}))) (N) = 0))$
111	32	nn0zd	$⊢ φ \to N - 1 \in ℤ$
112		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
113		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
114	111 112 113	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
115	39 114	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
116		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 \dots N - 1) \subseteq (0 \dots N)$
117	115 116	syl	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
118	117	sselda	$⊢ (φ \land j \in (0 \dots N - 1)) \to j \in (0 \dots N)$
119	91	adantr	$⊢ (φ \land j \in (0 \dots N)) \to N \in (1 \dots N)$
120	2	ffnd	$⊢ φ \to T Fn (1 \dots N)$
121	120	adantr	$⊢ (φ \land j \in (0 \dots N)) \to T Fn (1 \dots N)$
122	84	fconst	$⊢ (U [(1 \dots j)] \times \{1\}) : U [(1 \dots j)] ⟶ \{1\}$
123		c0ex	$⊢ 0 \in V$
124	123	fconst	$⊢ (U [(j + 1 \dots N)] \times \{0\}) : U [(j + 1 \dots N)] ⟶ \{0\}$
125	122 124	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\})$
126		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})$
127	126	simprbi	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun U^{-1}$
128		imain	$⊢ Fun U^{-1} \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [(1 \dots j)] \cap U [(j + 1 \dots N)]$
129	3 127 128	3syl	$⊢ φ \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [(1 \dots j)] \cap U [(j + 1 \dots N)]$
130		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
131	130	zred	$⊢ j \in (0 \dots N) \to j \in ℝ$
132	131	ltp1d	$⊢ j \in (0 \dots N) \to j < j + 1$
133		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
134	132 133	syl	$⊢ j \in (0 \dots N) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
135	134	imaeq2d	$⊢ j \in (0 \dots N) \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [\emptyset]$
136	135 61	eqtrdi	$⊢ j \in (0 \dots N) \to U [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
137	129 136	sylan9req	$⊢ (φ \land j \in (0 \dots N)) \to U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset$
138		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\}$
139	125 137 138	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\}$
140		elfznn0	$⊢ j \in (0 \dots N) \to j \in ℕ_{0}$
141	140 76	syl	$⊢ j \in (0 \dots N) \to j + 1 \in ℕ$
142		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
143	141 142	eleqtrdi	$⊢ j \in (0 \dots N) \to j + 1 \in ℤ_{\geq 1}$
144		elfzuz3	$⊢ j \in (0 \dots N) \to N \in ℤ_{\geq j}$
145		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq j}) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
146	143 144 145	syl2anc	$⊢ j \in (0 \dots N) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
147	146	imaeq2d	$⊢ j \in (0 \dots N) \to U [(1 \dots N)] = U [(1 \dots j) \cup (j + 1 \dots N)]$
148		imaundi	$⊢ U [(1 \dots j) \cup (j + 1 \dots N)] = U [(1 \dots j)] \cup U [(j + 1 \dots N)]$
149	147 148	eqtr2di	$⊢ j \in (0 \dots N) \to U [(1 \dots j)] \cup U [(j + 1 \dots N)] = U [(1 \dots N)]$
150	149 52	sylan9eqr	$⊢ (φ \land j \in (0 \dots N)) \to U [(1 \dots j)] \cup U [(j + 1 \dots N)] = (1 \dots N)$
151	150	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\})$
152	139 151	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\}$
153	152	ffnd	$⊢ (φ \land j \in (0 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
154		ovexd	$⊢ (φ \land j \in (0 \dots N)) \to (1 \dots N) \in V$
155		eqidd	$⊢ ((φ \land j \in (0 \dots N)) \land N \in (1 \dots N)) \to T (N) = T (N)$
156		eqidd	$⊢ ((φ \land j \in (0 \dots N)) \land N \in (1 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
157	121 153 154 154 88 155 156	ofval	$⊢ ((φ \land j \in (0 \dots N)) \land N \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = T (N) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
158	119 157	mpdan	$⊢ (φ \land j \in (0 \dots N)) \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = T (N) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
159	158	eqeq1d	$⊢ (φ \land j \in (0 \dots N)) \to ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow T (N) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
160	2 91	ffvelcdmd	$⊢ φ \to T (N) \in (0 ..^K)$
161		elfzonn0	$⊢ T (N) \in (0 ..^K) \to T (N) \in ℕ_{0}$
162	160 161	syl	$⊢ φ \to T (N) \in ℕ_{0}$
163	162	nn0red	$⊢ φ \to T (N) \in ℝ$
164	163	adantr	$⊢ (φ \land j \in (0 \dots N)) \to T (N) \in ℝ$
165	162	nn0ge0d	$⊢ φ \to 0 \leq T (N)$
166	165	adantr	$⊢ (φ \land j \in (0 \dots N)) \to 0 \leq T (N)$
167		1re	$⊢ 1 \in ℝ$
168		snssi	$⊢ 1 \in ℝ \to \{1\} \subseteq ℝ$
169	167 168	ax-mp	$⊢ \{1\} \subseteq ℝ$
170		0re	$⊢ 0 \in ℝ$
171		snssi	$⊢ 0 \in ℝ \to \{0\} \subseteq ℝ$
172	170 171	ax-mp	$⊢ \{0\} \subseteq ℝ$
173	169 172	unssi	$⊢ \{1\} \cup \{0\} \subseteq ℝ$
174	152 119	ffvelcdmd	$⊢ (φ \land j \in (0 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in (\{1\} \cup \{0\})$
175	173 174	sselid	$⊢ (φ \land j \in (0 \dots N)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in ℝ$
176		elun	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in (\{1\} \cup \{0\}) \leftrightarrow (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{1\} \lor ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{0\})$
177		0le1	$⊢ 0 \leq 1$
178		elsni	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{1\} \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 1$
179	177 178	breqtrrid	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{1\} \to 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
180		0le0	$⊢ 0 \leq 0$
181		elsni	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{0\} \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
182	180 181	breqtrrid	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{0\} \to 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
183	179 182	jaoi	$⊢ (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{1\} \lor ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in \{0\}) \to 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
184	176 183	sylbi	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in (\{1\} \cup \{0\}) \to 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
185	174 184	syl	$⊢ (φ \land j \in (0 \dots N)) \to 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N)$
186		add20	$⊢ ((T (N) \in ℝ \land 0 \leq T (N)) \land (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \in ℝ \land 0 \leq ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N))) \to (T (N) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0 \leftrightarrow (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
187	164 166 175 185 186	syl22anc	$⊢ (φ \land j \in (0 \dots N)) \to (T (N) + ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0 \leftrightarrow (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
188	159 187	bitrd	$⊢ (φ \land j \in (0 \dots N)) \to ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
189	118 188	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\}))) (N) = 0 \leftrightarrow (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
190	189	ralbidva	$⊢ φ \to (\forall j \in (0 \dots N - 1) (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow \forall j \in (0 \dots N - 1) (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
191	190	adantr	$⊢ (φ \land V = N) \to (\forall j \in (0 \dots N - 1) (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow \forall j \in (0 \dots N - 1) (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
192		breq2	$⊢ V = N \to (y < V \leftrightarrow y < N)$
193	192	ifbid	$⊢ V = N \to if (y < V, y, y + 1) = if (y < N, y, y + 1)$
194		elfzelz	$⊢ y \in (0 \dots N - 1) \to y \in ℤ$
195	194	zred	$⊢ y \in (0 \dots N - 1) \to y \in ℝ$
196	195	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \in ℝ$
197	32	nn0red	$⊢ φ \to N - 1 \in ℝ$
198	197	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 \in ℝ$
199	25	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℝ$
200		elfzle2	$⊢ y \in (0 \dots N - 1) \to y \leq N - 1$
201	200	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \leq N - 1$
202	25	ltm1d	$⊢ φ \to N - 1 < N$
203	202	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 < N$
204	196 198 199 201 203	lelttrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to y < N$
205	204	iftrued	$⊢ (φ \land y \in (0 \dots N - 1)) \to if (y < N, y, y + 1) = y$
206	193 205	sylan9eqr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land V = N) \to if (y < V, y, y + 1) = y$
207	206	an32s	$⊢ ((φ \land V = N) \land y \in (0 \dots N - 1)) \to if (y < V, y, y + 1) = y$
208	207	csbeq1d	$⊢ ((φ \land V = N) \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\}))) = ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
209	208	fveq1d	$⊢ ((φ \land V = N) \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\}))) (N) = ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N)$
210	209	eqeq1d	$⊢ ((φ \land V = N) \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\}))) (N) = 0 \leftrightarrow ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
211	210	ralbidva	$⊢ (φ \land V = N) \to (\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\}))) (N) = 0 \leftrightarrow \forall y \in (0 \dots N - 1) ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
212		nfv	$⊢ Ⅎ y (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
213		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
214		nfcv	$⊢ \underline{Ⅎ} j N$
215	213 214	nffv	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N)$
216	215	nfeq1	$⊢ Ⅎ j ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
217		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\})))$
218	217	fveq1d	$⊢ j = y \to (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N)$
219	218	eqeq1d	$⊢ j = y \to ((T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
220	212 216 219	cbvralw	$⊢ \forall j \in (0 \dots N - 1) (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0 \leftrightarrow \forall y \in (0 \dots N - 1) ⦋ y / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0$
221	211 220	bitr4di	$⊢ (φ \land V = N) \to (\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\}))) (N) = 0 \leftrightarrow \forall j \in (0 \dots N - 1) (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) (N) = 0)$
222		ne0i	$⊢ N - 1 \in (0 \dots N - 1) \to (0 \dots N - 1) \neq \emptyset$
223		r19.3rzv	$⊢ (0 \dots N - 1) \neq \emptyset \to (T (N) = 0 \leftrightarrow \forall j \in (0 \dots N - 1) T (N) = 0)$
224	34 222 223	3syl	$⊢ φ \to (T (N) = 0 \leftrightarrow \forall j \in (0 \dots N - 1) T (N) = 0)$
225		elfzelz	$⊢ j \in (0 \dots N - 1) \to j \in ℤ$
226	225	zred	$⊢ j \in (0 \dots N - 1) \to j \in ℝ$
227	226	ltp1d	$⊢ j \in (0 \dots N - 1) \to j < j + 1$
228	227 133	syl	$⊢ j \in (0 \dots N - 1) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
229	228	imaeq2d	$⊢ j \in (0 \dots N - 1) \to U [(1 \dots j) \cap (j + 1 \dots N)] = U [\emptyset]$
230	229 61	eqtrdi	$⊢ j \in (0 \dots N - 1) \to U [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
231	129 230	sylan9req	$⊢ (φ \land j \in (0 \dots N - 1)) \to U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset$
232	231	adantlr	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset$
233		simplr	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to U (N) = N$
234		f1ofn	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U Fn (1 \dots N)$
235	3 234	syl	$⊢ φ \to U Fn (1 \dots N)$
236	235	adantr	$⊢ (φ \land j \in (0 \dots N - 1)) \to U Fn (1 \dots N)$
237		elfznn0	$⊢ j \in (0 \dots N - 1) \to j \in ℕ_{0}$
238	237 76	syl	$⊢ j \in (0 \dots N - 1) \to j + 1 \in ℕ$
239	238 142	eleqtrdi	$⊢ j \in (0 \dots N - 1) \to j + 1 \in ℤ_{\geq 1}$
240		fzss1	$⊢ j + 1 \in ℤ_{\geq 1} \to (j + 1 \dots N) \subseteq (1 \dots N)$
241	239 240	syl	$⊢ j \in (0 \dots N - 1) \to (j + 1 \dots N) \subseteq (1 \dots N)$
242	241	adantl	$⊢ (φ \land j \in (0 \dots N - 1)) \to (j + 1 \dots N) \subseteq (1 \dots N)$
243	39	adantr	$⊢ (φ \land j \in (0 \dots N - 1)) \to N - 1 + 1 = N$
244		elfzuz3	$⊢ j \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq j}$
245		eluzp1p1	$⊢ N - 1 \in ℤ_{\geq j} \to N - 1 + 1 \in ℤ_{\geq (j + 1)}$
246	244 245	syl	$⊢ j \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq (j + 1)}$
247	246	adantl	$⊢ (φ \land j \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq (j + 1)}$
248	243 247	eqeltrrd	$⊢ (φ \land j \in (0 \dots N - 1)) \to N \in ℤ_{\geq (j + 1)}$
249		eluzfz2	$⊢ N \in ℤ_{\geq (j + 1)} \to N \in (j + 1 \dots N)$
250	248 249	syl	$⊢ (φ \land j \in (0 \dots N - 1)) \to N \in (j + 1 \dots N)$
251		fnfvima	$⊢ (U Fn (1 \dots N) \land (j + 1 \dots N) \subseteq (1 \dots N) \land N \in (j + 1 \dots N)) \to U (N) \in U [(j + 1 \dots N)]$
252	236 242 250 251	syl3anc	$⊢ (φ \land j \in (0 \dots N - 1)) \to U (N) \in U [(j + 1 \dots N)]$
253	252	adantlr	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to U (N) \in U [(j + 1 \dots N)]$
254	233 253	eqeltrrd	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to N \in U [(j + 1 \dots N)]$
255		fnconstg	$⊢ 1 \in V \to (U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)]$
256	84 255	ax-mp	$⊢ (U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)]$
257		fnconstg	$⊢ 0 \in V \to (U [(j + 1 \dots N)] \times \{0\}) Fn U [(j + 1 \dots N)]$
258	123 257	ax-mp	$⊢ (U [(j + 1 \dots N)] \times \{0\}) Fn U [(j + 1 \dots N)]$
259		fvun2	$⊢ ((U [(1 \dots j)] \times \{1\}) Fn U [(1 \dots j)] \land (U [(j + 1 \dots N)] \times \{0\}) Fn U [(j + 1 \dots N)] \land (U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset \land N \in U [(j + 1 \dots N)])) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = (U [(j + 1 \dots N)] \times \{0\}) (N)$
260	256 258 259	mp3an12	$⊢ (U [(1 \dots j)] \cap U [(j + 1 \dots N)] = \emptyset \land N \in U [(j + 1 \dots N)]) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = (U [(j + 1 \dots N)] \times \{0\}) (N)$
261	232 254 260	syl2anc	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = (U [(j + 1 \dots N)] \times \{0\}) (N)$
262	123	fvconst2	$⊢ N \in U [(j + 1 \dots N)] \to (U [(j + 1 \dots N)] \times \{0\}) (N) = 0$
263	254 262	syl	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to (U [(j + 1 \dots N)] \times \{0\}) (N) = 0$
264	261 263	eqtrd	$⊢ ((φ \land U (N) = N) \land j \in (0 \dots N - 1)) \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
265	264	ralrimiva	$⊢ (φ \land U (N) = N) \to \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
266	265	ex	$⊢ φ \to (U (N) = N \to \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
267	34	adantr	$⊢ (φ \land U (N) \neq N) \to N - 1 \in (0 \dots N - 1)$
268		ax-1ne0	$⊢ 1 \neq 0$
269		imain	$⊢ Fun U^{-1} \to U [(1 \dots N - 1) \cap (N - 1 + 1 \dots N)] = U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)]$
270	3 127 269	3syl	$⊢ φ \to U [(1 \dots N - 1) \cap (N - 1 + 1 \dots N)] = U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)]$
271	202 39	breqtrrd	$⊢ φ \to N - 1 < N - 1 + 1$
272		fzdisj	$⊢ N - 1 < N - 1 + 1 \to (1 \dots N - 1) \cap (N - 1 + 1 \dots N) = \emptyset$
273	271 272	syl	$⊢ φ \to (1 \dots N - 1) \cap (N - 1 + 1 \dots N) = \emptyset$
274	273	imaeq2d	$⊢ φ \to U [(1 \dots N - 1) \cap (N - 1 + 1 \dots N)] = U [\emptyset]$
275	274 61	eqtrdi	$⊢ φ \to U [(1 \dots N - 1) \cap (N - 1 + 1 \dots N)] = \emptyset$
276	270 275	eqtr3d	$⊢ φ \to U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)] = \emptyset$
277	276	adantr	$⊢ (φ \land U (N) \neq N) \to U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)] = \emptyset$
278	91	adantr	$⊢ (φ \land U (N) \neq N) \to N \in (1 \dots N)$
279		elimasni	$⊢ N \in U [\{N\}] \to N U N$
280		fnbrfvb	$⊢ (U Fn (1 \dots N) \land N \in (1 \dots N)) \to (U (N) = N \leftrightarrow N U N)$
281	235 91 280	syl2anc	$⊢ φ \to (U (N) = N \leftrightarrow N U N)$
282	279 281	imbitrrid	$⊢ φ \to (N \in U [\{N\}] \to U (N) = N)$
283	282	necon3ad	$⊢ φ \to (U (N) \neq N \to \neg N \in U [\{N\}])$
284	283	imp	$⊢ (φ \land U (N) \neq N) \to \neg N \in U [\{N\}]$
285	278 284	eldifd	$⊢ (φ \land U (N) \neq N) \to N \in ((1 \dots N) ∖ U [\{N\}])$
286		imadif	$⊢ Fun U^{-1} \to U [(1 \dots N) ∖ \{N\}] = U [(1 \dots N)] ∖ U [\{N\}]$
287	3 127 286	3syl	$⊢ φ \to U [(1 \dots N) ∖ \{N\}] = U [(1 \dots N)] ∖ U [\{N\}]$
288		difun2	$⊢ ((1 \dots N - 1) \cup \{N\}) ∖ \{N\} = (1 \dots N - 1) ∖ \{N\}$
289		elun	$⊢ j \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow (j \in (1 \dots N - 1) \lor j \in \{N\})$
290		velsn	$⊢ j \in \{N\} \leftrightarrow j = N$
291	290	orbi2i	$⊢ (j \in (1 \dots N - 1) \lor j \in \{N\}) \leftrightarrow (j \in (1 \dots N - 1) \lor j = N)$
292	289 291	bitri	$⊢ j \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow (j \in (1 \dots N - 1) \lor j = N)$
293	1 142	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
294		fzm1	$⊢ N \in ℤ_{\geq 1} \to (j \in (1 \dots N) \leftrightarrow (j \in (1 \dots N - 1) \lor j = N))$
295	293 294	syl	$⊢ φ \to (j \in (1 \dots N) \leftrightarrow (j \in (1 \dots N - 1) \lor j = N))$
296	292 295	bitr4id	$⊢ φ \to (j \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow j \in (1 \dots N))$
297	296	eqrdv	$⊢ φ \to (1 \dots N - 1) \cup \{N\} = (1 \dots N)$
298	297	difeq1d	$⊢ φ \to ((1 \dots N - 1) \cup \{N\}) ∖ \{N\} = (1 \dots N) ∖ \{N\}$
299	197 25	ltnled	$⊢ φ \to (N - 1 < N \leftrightarrow \neg N \leq N - 1)$
300	202 299	mpbid	$⊢ φ \to \neg N \leq N - 1$
301		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
302	300 301	nsyl	$⊢ φ \to \neg N \in (1 \dots N - 1)$
303		difsn	$⊢ \neg N \in (1 \dots N - 1) \to (1 \dots N - 1) ∖ \{N\} = (1 \dots N - 1)$
304	302 303	syl	$⊢ φ \to (1 \dots N - 1) ∖ \{N\} = (1 \dots N - 1)$
305	288 298 304	3eqtr3a	$⊢ φ \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
306	305	imaeq2d	$⊢ φ \to U [(1 \dots N) ∖ \{N\}] = U [(1 \dots N - 1)]$
307	52	difeq1d	$⊢ φ \to U [(1 \dots N)] ∖ U [\{N\}] = (1 \dots N) ∖ U [\{N\}]$
308	287 306 307	3eqtr3rd	$⊢ φ \to (1 \dots N) ∖ U [\{N\}] = U [(1 \dots N - 1)]$
309	308	adantr	$⊢ (φ \land U (N) \neq N) \to (1 \dots N) ∖ U [\{N\}] = U [(1 \dots N - 1)]$
310	285 309	eleqtrd	$⊢ (φ \land U (N) \neq N) \to N \in U [(1 \dots N - 1)]$
311		fnconstg	$⊢ 1 \in V \to (U [(1 \dots N - 1)] \times \{1\}) Fn U [(1 \dots N - 1)]$
312	84 311	ax-mp	$⊢ (U [(1 \dots N - 1)] \times \{1\}) Fn U [(1 \dots N - 1)]$
313		fnconstg	$⊢ 0 \in V \to (U [(N - 1 + 1 \dots N)] \times \{0\}) Fn U [(N - 1 + 1 \dots N)]$
314	123 313	ax-mp	$⊢ (U [(N - 1 + 1 \dots N)] \times \{0\}) Fn U [(N - 1 + 1 \dots N)]$
315		fvun1	$⊢ ((U [(1 \dots N - 1)] \times \{1\}) Fn U [(1 \dots N - 1)] \land (U [(N - 1 + 1 \dots N)] \times \{0\}) Fn U [(N - 1 + 1 \dots N)] \land (U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)] = \emptyset \land N \in U [(1 \dots N - 1)])) \to ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) = (U [(1 \dots N - 1)] \times \{1\}) (N)$
316	312 314 315	mp3an12	$⊢ (U [(1 \dots N - 1)] \cap U [(N - 1 + 1 \dots N)] = \emptyset \land N \in U [(1 \dots N - 1)]) \to ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) = (U [(1 \dots N - 1)] \times \{1\}) (N)$
317	277 310 316	syl2anc	$⊢ (φ \land U (N) \neq N) \to ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) = (U [(1 \dots N - 1)] \times \{1\}) (N)$
318	84	fvconst2	$⊢ N \in U [(1 \dots N - 1)] \to (U [(1 \dots N - 1)] \times \{1\}) (N) = 1$
319	310 318	syl	$⊢ (φ \land U (N) \neq N) \to (U [(1 \dots N - 1)] \times \{1\}) (N) = 1$
320	317 319	eqtrd	$⊢ (φ \land U (N) \neq N) \to ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) = 1$
321	320	neeq1d	$⊢ (φ \land U (N) \neq N) \to (((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) \neq 0 \leftrightarrow 1 \neq 0)$
322	268 321	mpbiri	$⊢ (φ \land U (N) \neq N) \to ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) \neq 0$
323		df-ne	$⊢ ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \neq 0 \leftrightarrow \neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
324		oveq2	$⊢ j = N - 1 \to (1 \dots j) = (1 \dots N - 1)$
325	324	imaeq2d	$⊢ j = N - 1 \to U [(1 \dots j)] = U [(1 \dots N - 1)]$
326	325	xpeq1d	$⊢ j = N - 1 \to U [(1 \dots j)] \times \{1\} = U [(1 \dots N - 1)] \times \{1\}$
327		oveq1	$⊢ j = N - 1 \to j + 1 = N - 1 + 1$
328	327	oveq1d	$⊢ j = N - 1 \to (j + 1 \dots N) = (N - 1 + 1 \dots N)$
329	328	imaeq2d	$⊢ j = N - 1 \to U [(j + 1 \dots N)] = U [(N - 1 + 1 \dots N)]$
330	329	xpeq1d	$⊢ j = N - 1 \to U [(j + 1 \dots N)] \times \{0\} = U [(N - 1 + 1 \dots N)] \times \{0\}$
331	326 330	uneq12d	$⊢ j = N - 1 \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})$
332	331	fveq1d	$⊢ j = N - 1 \to ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N)$
333	332	neeq1d	$⊢ j = N - 1 \to (((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) \neq 0 \leftrightarrow ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) \neq 0)$
334	323 333	bitr3id	$⊢ j = N - 1 \to (\neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0 \leftrightarrow ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) \neq 0)$
335	334	rspcev	$⊢ (N - 1 \in (0 \dots N - 1) \land ((U [(1 \dots N - 1)] \times \{1\}) \cup (U [(N - 1 + 1 \dots N)] \times \{0\})) (N) \neq 0) \to \exists j \in (0 \dots N - 1) \neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
336	267 322 335	syl2anc	$⊢ (φ \land U (N) \neq N) \to \exists j \in (0 \dots N - 1) \neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
337	336	ex	$⊢ φ \to (U (N) \neq N \to \exists j \in (0 \dots N - 1) \neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
338		rexnal	$⊢ \exists j \in (0 \dots N - 1) \neg ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0 \leftrightarrow \neg \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0$
339	337 338	imbitrdi	$⊢ φ \to (U (N) \neq N \to \neg \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
340	339	necon4ad	$⊢ φ \to (\forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0 \to U (N) = N)$
341	266 340	impbid	$⊢ φ \to (U (N) = N \leftrightarrow \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
342	224 341	anbi12d	$⊢ φ \to ((T (N) = 0 \land U (N) = N) \leftrightarrow (\forall j \in (0 \dots N - 1) T (N) = 0 \land \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
343		r19.26	$⊢ \forall j \in (0 \dots N - 1) (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0) \leftrightarrow (\forall j \in (0 \dots N - 1) T (N) = 0 \land \forall j \in (0 \dots N - 1) ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0)$
344	342 343	bitr4di	$⊢ φ \to ((T (N) = 0 \land U (N) = N) \leftrightarrow \forall j \in (0 \dots N - 1) (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
345	344	adantr	$⊢ (φ \land V = N) \to ((T (N) = 0 \land U (N) = N) \leftrightarrow \forall j \in (0 \dots N - 1) (T (N) = 0 \land ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) (N) = 0))$
346	191 221 345	3bitr4d	$⊢ (φ \land V = N) \to (\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\}))) (N) = 0 \leftrightarrow (T (N) = 0 \land U (N) = N))$
347	346	pm5.32da	$⊢ φ \to ((V = N \land \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\}))) (N) = 0) \leftrightarrow (V = N \land (T (N) = 0 \land U (N) = N)))$
348	110 347	bitrd	$⊢ φ \to (\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\}))) (N) = 0 \leftrightarrow (V = N \land (T (N) = 0 \land U (N) = N)))$
349	348	notbid	$⊢ φ \to (\neg \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\}))) (N) = 0 \leftrightarrow \neg (V = N \land (T (N) = 0 \land U (N) = N)))$
350	16 349	bitrid	$⊢ φ \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)))$

Metamath Proof Explorer

Theorem poimirlem23

Proof