poimirlem25

Description: Lemma for poimir stating that for a given simplex such that no vertex maps to N , the number of admissible faces is even. (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)$
	poimirlem25.5	$⊢ (φ \land j \in (0 \dots N)) \to N \neq ⦋ ⟨T, U⟩ / s ⦌ C$
Assertion	poimirlem25	$⊢ φ \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$

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		poimirlem25.5	$⊢ (φ \land j \in (0 \dots N)) \to N \neq ⦋ ⟨T, U⟩ / s ⦌ C$
7		neq0	$⊢ \neg \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} = \emptyset \leftrightarrow \exists t t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}$
8		2z	$⊢ 2 \in ℤ$
9		iddvds	$⊢ 2 \in ℤ \to 2 ∥ 2$
10	8 9	ax-mp	$⊢ 2 ∥ 2$
11		df-2	$⊢ 2 = 1 + 1$
12	10 11	breqtri	$⊢ 2 ∥ (1 + 1)$
13		vex	$⊢ t \in V$
14		fzfi	$⊢ (0 \dots N) \in Fin$
15		rabfi	$⊢ (0 \dots N) \in Fin \to \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \in Fin$
16	14 15	ax-mp	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \in Fin$
17		diffi	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \in Fin \to \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\} \in Fin$
18	16 17	ax-mp	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\} \in Fin$
19		neldifsn	$⊢ \neg t \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\})$
20	18 19	pm3.2i	$⊢ (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\} \in Fin \land \neg t \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}))$
21		hashunsng	$⊢ t \in V \to ((\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\} \in Fin \land \neg t \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\})) \to \|(\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}) \cup \{t\}\| = \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| + 1)$
22	13 20 21	mp2	$⊢ \|(\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}) \cup \{t\}\| = \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| + 1$
23		difsnid	$⊢ t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \to (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}) \cup \{t\} = \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}$
24	23	fveq2d	$⊢ t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \to \|(\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}) \cup \{t\}\| = \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$
25	22 24	eqtr3id	$⊢ t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| + 1 = \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$
26	25	adantl	$⊢ (φ \land t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}) \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| + 1 = \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$
27		sneq	$⊢ y = t \to \{y\} = \{t\}$
28	27	difeq2d	$⊢ y = t \to (0 \dots N) ∖ \{y\} = (0 \dots N) ∖ \{t\}$
29	28	rexeqdv	$⊢ y = t \to (\exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
30	29	ralbidv	$⊢ y = t \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
31	30	elrab	$⊢ t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \leftrightarrow (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
32	6	ralrimiva	$⊢ φ \to \forall j \in (0 \dots N) N \neq ⦋ ⟨T, U⟩ / s ⦌ C$
33		nfcv	$⊢ \underline{Ⅎ} j N$
34		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
35	33 34	nfne	$⊢ Ⅎ j N \neq ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
36		csbeq1a	$⊢ j = t \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
37	36	neeq2d	$⊢ j = t \to (N \neq ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow N \neq ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
38	35 37	rspc	$⊢ t \in (0 \dots N) \to (\forall j \in (0 \dots N) N \neq ⦋ ⟨T, U⟩ / s ⦌ C \to N \neq ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
39	32 38	mpan9	$⊢ (φ \land t \in (0 \dots N)) \to N \neq ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
40		nesym	$⊢ N \neq ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N$
41	39 40	sylib	$⊢ (φ \land t \in (0 \dots N)) \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N$
42		nfv	$⊢ Ⅎ j (φ \land t \in (0 \dots N))$
43	34	nfel1	$⊢ Ⅎ j ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)$
44	42 43	nfim	$⊢ Ⅎ j ((φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N))$
45		eleq1w	$⊢ j = t \to (j \in (0 \dots N) \leftrightarrow t \in (0 \dots N))$
46	45	anbi2d	$⊢ j = t \to ((φ \land j \in (0 \dots N)) \leftrightarrow (φ \land t \in (0 \dots N)))$
47	36	eleq1d	$⊢ j = t \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N))$
48	46 47	imbi12d	$⊢ j = t \to (((φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)) \leftrightarrow ((φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)))$
49		ovex	$⊢ (0 ..^K) \in V$
50		ovex	$⊢ (1 \dots N) \in V$
51	49 50	elmap	$⊢ T \in ({(0 ..^K)}^{(1 \dots N)}) \leftrightarrow T : (1 \dots N) ⟶ (0 ..^K)$
52	4 51	sylibr	$⊢ φ \to T \in ({(0 ..^K)}^{(1 \dots N)})$
53		fzfi	$⊢ (1 \dots N) \in Fin$
54		f1oexrnex	$⊢ (U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land (1 \dots N) \in Fin) \to U \in V$
55	53 54	mpan2	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U \in V$
56		f1oeq1	$⊢ f = U \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
57	56	elabg	$⊢ U \in V \to (U \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
58	55 57	syl	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to (U \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
59	58	ibir	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
60	5 59	syl	$⊢ φ \to U \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
61		opelxpi	$⊢ (T \in ({(0 ..^K)}^{(1 \dots N)}) \land U \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ⟨T, U⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
62	52 60 61	syl2anc	$⊢ φ \to ⟨T, U⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
63	62	adantr	$⊢ (φ \land j \in (0 \dots N)) \to ⟨T, U⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
64		nfcv	$⊢ \underline{Ⅎ} s ⟨T, U⟩$
65		nfv	$⊢ Ⅎ s (φ \land j \in (0 \dots N))$
66		nfcsb1v	$⊢ \underline{Ⅎ} s ⦋ ⟨T, U⟩ / s ⦌ C$
67	66	nfel1	$⊢ Ⅎ s ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)$
68	65 67	nfim	$⊢ Ⅎ s ((φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N))$
69		csbeq1a	$⊢ s = ⟨T, U⟩ \to C = ⦋ ⟨T, U⟩ / s ⦌ C$
70	69	eleq1d	$⊢ s = ⟨T, U⟩ \to (C \in (0 \dots N) \leftrightarrow ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N))$
71	70	imbi2d	$⊢ s = ⟨T, U⟩ \to (((φ \land j \in (0 \dots N)) \to C \in (0 \dots N)) \leftrightarrow ((φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)))$
72		elun	$⊢ p \in (\{1\} \cup \{0\}) \leftrightarrow (p \in \{1\} \lor p \in \{0\})$
73		fzofzp1	$⊢ i \in (0 ..^K) \to i + 1 \in (0 \dots K)$
74		elsni	$⊢ p \in \{1\} \to p = 1$
75	74	oveq2d	$⊢ p \in \{1\} \to i + p = i + 1$
76	75	eleq1d	$⊢ p \in \{1\} \to (i + p \in (0 \dots K) \leftrightarrow i + 1 \in (0 \dots K))$
77	73 76	syl5ibrcom	$⊢ i \in (0 ..^K) \to (p \in \{1\} \to i + p \in (0 \dots K))$
78		elfzonn0	$⊢ i \in (0 ..^K) \to i \in ℕ_{0}$
79	78	nn0cnd	$⊢ i \in (0 ..^K) \to i \in ℂ$
80	79	addid1d	$⊢ i \in (0 ..^K) \to i + 0 = i$
81		elfzofz	$⊢ i \in (0 ..^K) \to i \in (0 \dots K)$
82	80 81	eqeltrd	$⊢ i \in (0 ..^K) \to i + 0 \in (0 \dots K)$
83		elsni	$⊢ p \in \{0\} \to p = 0$
84	83	oveq2d	$⊢ p \in \{0\} \to i + p = i + 0$
85	84	eleq1d	$⊢ p \in \{0\} \to (i + p \in (0 \dots K) \leftrightarrow i + 0 \in (0 \dots K))$
86	82 85	syl5ibrcom	$⊢ i \in (0 ..^K) \to (p \in \{0\} \to i + p \in (0 \dots K))$
87	77 86	jaod	$⊢ i \in (0 ..^K) \to ((p \in \{1\} \lor p \in \{0\}) \to i + p \in (0 \dots K))$
88	72 87	syl5bi	$⊢ i \in (0 ..^K) \to (p \in (\{1\} \cup \{0\}) \to i + p \in (0 \dots K))$
89	88	imp	$⊢ (i \in (0 ..^K) \land p \in (\{1\} \cup \{0\})) \to i + p \in (0 \dots K)$
90	89	adantl	$⊢ ((s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N)) \land (i \in (0 ..^K) \land p \in (\{1\} \cup \{0\}))) \to i + p \in (0 \dots K)$
91		xp1st	$⊢ s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (s) \in ({(0 ..^K)}^{(1 \dots N)})$
92		elmapi	$⊢ 1^{st} (s) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (s) : (1 \dots N) ⟶ (0 ..^K)$
93	91 92	syl	$⊢ s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (s) : (1 \dots N) ⟶ (0 ..^K)$
94	93	adantr	$⊢ (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N)) \to 1^{st} (s) : (1 \dots N) ⟶ (0 ..^K)$
95		xp2nd	$⊢ s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (s) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
96		fvex	$⊢ 2^{nd} (s) \in V$
97		f1oeq1	$⊢ f = 2^{nd} (s) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
98	96 97	elab	$⊢ 2^{nd} (s) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
99	95 98	sylib	$⊢ s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
100		1ex	$⊢ 1 \in V$
101	100	fconst	$⊢ (2^{nd} (s) [(1 \dots j)] \times \{1\}) : 2^{nd} (s) [(1 \dots j)] ⟶ \{1\}$
102		c0ex	$⊢ 0 \in V$
103	102	fconst	$⊢ (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{0\}$
104	101 103	pm3.2i	$⊢ ((2^{nd} (s) [(1 \dots j)] \times \{1\}) : 2^{nd} (s) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{0\})$
105		dff1o3	$⊢ 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (s) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (s)}^{-1})$
106		imain	$⊢ Fun {2^{nd} (s)}^{-1} \to 2^{nd} (s) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (s) [(1 \dots j)] \cap 2^{nd} (s) [(j + 1 \dots N)]$
107	105 106	simplbiim	$⊢ 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (s) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (s) [(1 \dots j)] \cap 2^{nd} (s) [(j + 1 \dots N)]$
108		elfznn0	$⊢ j \in (0 \dots N) \to j \in ℕ_{0}$
109	108	nn0red	$⊢ j \in (0 \dots N) \to j \in ℝ$
110	109	ltp1d	$⊢ j \in (0 \dots N) \to j < j + 1$
111		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
112	110 111	syl	$⊢ j \in (0 \dots N) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
113	112	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (s) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (s) [\emptyset]$
114		ima0	$⊢ 2^{nd} (s) [\emptyset] = \emptyset$
115	113 114	eqtrdi	$⊢ j \in (0 \dots N) \to 2^{nd} (s) [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
116	107 115	sylan9req	$⊢ (2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (0 \dots N)) \to 2^{nd} (s) [(1 \dots j)] \cap 2^{nd} (s) [(j + 1 \dots N)] = \emptyset$
117		fun	$⊢ (((2^{nd} (s) [(1 \dots j)] \times \{1\}) : 2^{nd} (s) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{0\}) \land 2^{nd} (s) [(1 \dots j)] \cap 2^{nd} (s) [(j + 1 \dots N)] = \emptyset) \to ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
118	104 116 117	sylancr	$⊢ (2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (0 \dots N)) \to ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
119		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
120	108 119	syl	$⊢ j \in (0 \dots N) \to j + 1 \in ℕ$
121		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
122	120 121	eleqtrdi	$⊢ j \in (0 \dots N) \to j + 1 \in ℤ_{\geq 1}$
123		elfzuz3	$⊢ j \in (0 \dots N) \to N \in ℤ_{\geq j}$
124		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq j}) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
125	122 123 124	syl2anc	$⊢ j \in (0 \dots N) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
126	125	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (s) [(1 \dots N)] = 2^{nd} (s) [(1 \dots j) \cup (j + 1 \dots N)]$
127		imaundi	$⊢ 2^{nd} (s) [(1 \dots j) \cup (j + 1 \dots N)] = 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)]$
128	126 127	eqtr2di	$⊢ j \in (0 \dots N) \to 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)] = 2^{nd} (s) [(1 \dots N)]$
129		f1ofo	$⊢ 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (s) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
130		foima	$⊢ 2^{nd} (s) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (s) [(1 \dots N)] = (1 \dots N)$
131	129 130	syl	$⊢ 2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (s) [(1 \dots N)] = (1 \dots N)$
132	128 131	sylan9eqr	$⊢ (2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (0 \dots N)) \to 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)] = (1 \dots N)$
133	132	feq2d	$⊢ (2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (0 \dots N)) \to (((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (s) [(1 \dots j)] \cup 2^{nd} (s) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\} \leftrightarrow ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\})$
134	118 133	mpbid	$⊢ (2^{nd} (s) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (0 \dots N)) \to ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
135	99 134	sylan	$⊢ (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N)) \to ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
136		fzfid	$⊢ (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N)) \to (1 \dots N) \in Fin$
137		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
138	90 94 135 136 136 137	off	$⊢ (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N)) \to (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)$
139		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$
140		feq1	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to (p : (1 \dots N) ⟶ (0 \dots K) \leftrightarrow (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K))$
141	140	anbi2d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to ((φ \land p : (1 \dots N) ⟶ (0 \dots K)) \leftrightarrow (φ \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)))$
142	2	eleq1d	$⊢ 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 \in (0 \dots N) \leftrightarrow C \in (0 \dots N))$
143	141 142	imbi12d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to (((φ \land p : (1 \dots N) ⟶ (0 \dots K)) \to B \in (0 \dots N)) \leftrightarrow ((φ \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)) \to C \in (0 \dots N)))$
144	139 143 3	vtocl	$⊢ (φ \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots K)) \to C \in (0 \dots N)$
145	138 144	sylan2	$⊢ (φ \land (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land j \in (0 \dots N))) \to C \in (0 \dots N)$
146	145	an12s	$⊢ (s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land (φ \land j \in (0 \dots N))) \to C \in (0 \dots N)$
147	146	ex	$⊢ s \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ((φ \land j \in (0 \dots N)) \to C \in (0 \dots N))$
148	64 68 71 147	vtoclgaf	$⊢ ⟨T, U⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ((φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N))$
149	63 148	mpcom	$⊢ (φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)$
150	44 48 149	chvarfv	$⊢ (φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N)$
151	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
152		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
153	151 152	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
154		fzm1	$⊢ N \in ℤ_{\geq 0} \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N))$
155	153 154	syl	$⊢ φ \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N))$
156	155	adantr	$⊢ (φ \land t \in (0 \dots N)) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N))$
157	150 156	mpbid	$⊢ (φ \land t \in (0 \dots N)) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N)$
158	157	ord	$⊢ (φ \land t \in (0 \dots N)) \to (\neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = N)$
159	41 158	mt3d	$⊢ (φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
160	159	adantrr	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
161		fzfi	$⊢ (0 \dots N - 1) \in Fin$
162	1	nncnd	$⊢ φ \to N \in ℂ$
163		1cnd	$⊢ φ \to 1 \in ℂ$
164	162 163 163	addsubd	$⊢ φ \to N + 1 - 1 = N - 1 + 1$
165		hashfz0	$⊢ N \in ℕ_{0} \to \|(0 \dots N)\| = N + 1$
166	151 165	syl	$⊢ φ \to \|(0 \dots N)\| = N + 1$
167	166	oveq1d	$⊢ φ \to \|(0 \dots N)\| - 1 = N + 1 - 1$
168		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
169		hashfz0	$⊢ N - 1 \in ℕ_{0} \to \|(0 \dots N - 1)\| = N - 1 + 1$
170	1 168 169	3syl	$⊢ φ \to \|(0 \dots N - 1)\| = N - 1 + 1$
171	164 167 170	3eqtr4rd	$⊢ φ \to \|(0 \dots N - 1)\| = \|(0 \dots N)\| - 1$
172		hashdifsn	$⊢ ((0 \dots N) \in Fin \land t \in (0 \dots N)) \to \|(0 \dots N) ∖ \{t\}\| = \|(0 \dots N)\| - 1$
173	14 172	mpan	$⊢ t \in (0 \dots N) \to \|(0 \dots N) ∖ \{t\}\| = \|(0 \dots N)\| - 1$
174	173	eqcomd	$⊢ t \in (0 \dots N) \to \|(0 \dots N)\| - 1 = \|(0 \dots N) ∖ \{t\}\|$
175	171 174	sylan9eq	$⊢ (φ \land t \in (0 \dots N)) \to \|(0 \dots N - 1)\| = \|(0 \dots N) ∖ \{t\}\|$
176		diffi	$⊢ (0 \dots N) \in Fin \to (0 \dots N) ∖ \{t\} \in Fin$
177	14 176	ax-mp	$⊢ (0 \dots N) ∖ \{t\} \in Fin$
178		hashen	$⊢ ((0 \dots N - 1) \in Fin \land (0 \dots N) ∖ \{t\} \in Fin) \to (\|(0 \dots N - 1)\| = \|(0 \dots N) ∖ \{t\}\| \leftrightarrow (0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\}))$
179	161 177 178	mp2an	$⊢ \|(0 \dots N - 1)\| = \|(0 \dots N) ∖ \{t\}\| \leftrightarrow (0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\})$
180	175 179	sylib	$⊢ (φ \land t \in (0 \dots N)) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\})$
181		phpreu	$⊢ ((0 \dots N - 1) \in Fin \land (0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\})) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
182	161 180 181	sylancr	$⊢ (φ \land t \in (0 \dots N)) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
183	182	biimpd	$⊢ (φ \land t \in (0 \dots N)) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \to \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
184	183	impr	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
185		nfv	$⊢ Ⅎ z i = ⦋ ⟨T, U⟩ / s ⦌ C$
186		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
187	186	nfeq2	$⊢ Ⅎ j i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
188		csbeq1a	$⊢ j = z \to ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
189	188	eqeq2d	$⊢ j = z \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
190	185 187 189	cbvreuw	$⊢ \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! z \in ((0 \dots N) ∖ \{t\}) i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
191		eqeq1	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
192	191	reubidv	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists! z \in ((0 \dots N) ∖ \{t\}) i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! z \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
193	190 192	syl5bb	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! z \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
194	193	rspcv	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \to (\forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists! z \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
195	160 184 194	sylc	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to \exists! z \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
196		an32	$⊢ ((t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \land z \in ((0 \dots N) ∖ \{t\})) \leftrightarrow ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
197	196	biimpi	$⊢ ((t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \land z \in ((0 \dots N) ∖ \{t\})) \to ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
198	197	adantll	$⊢ ((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \to ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
199		eqeq2	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
200		rexsns	$⊢ \exists j \in \{t\} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \underset{˙}{[} t / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C$
201	34	nfeq2	$⊢ Ⅎ j i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
202	36	eqeq2d	$⊢ j = t \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
203	201 202	sbciegf	$⊢ t \in V \to (\underset{˙}{[} t / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
204	13 203	ax-mp	$⊢ \underset{˙}{[} t / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
205	200 204	bitri	$⊢ \exists j \in \{t\} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
206		rexsns	$⊢ \exists j \in \{z\} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \underset{˙}{[} z / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C$
207		vex	$⊢ z \in V$
208	187 189	sbciegf	$⊢ z \in V \to (\underset{˙}{[} z / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
209	207 208	ax-mp	$⊢ \underset{˙}{[} z / j \underset{˙}{]} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
210	206 209	bitri	$⊢ \exists j \in \{z\} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow i = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
211	199 205 210	3bitr4g	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists j \in \{t\} i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in \{z\} i = ⦋ ⟨T, U⟩ / s ⦌ C)$
212	211	orbi1d	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to ((\exists j \in \{t\} i = ⦋ ⟨T, U⟩ / s ⦌ C \lor \exists j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (\exists j \in \{z\} i = ⦋ ⟨T, U⟩ / s ⦌ C \lor \exists j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C))$
213		rexun	$⊢ \exists j \in (\{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow (\exists j \in \{t\} i = ⦋ ⟨T, U⟩ / s ⦌ C \lor \exists j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
214		rexun	$⊢ \exists j \in (\{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow (\exists j \in \{z\} i = ⦋ ⟨T, U⟩ / s ⦌ C \lor \exists j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
215	212 213 214	3bitr4g	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists j \in (\{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in (\{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
216	215	adantl	$⊢ ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to (\exists j \in (\{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in (\{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
217		eldifsni	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to z \neq t$
218	217	necomd	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to t \neq z$
219		dif32	$⊢ ((0 \dots N) ∖ \{t\}) ∖ \{z\} = ((0 \dots N) ∖ \{z\}) ∖ \{t\}$
220	219	uneq2i	$⊢ \{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\}) = \{t\} \cup (((0 \dots N) ∖ \{z\}) ∖ \{t\})$
221		snssi	$⊢ t \in ((0 \dots N) ∖ \{z\}) \to \{t\} \subseteq (0 \dots N) ∖ \{z\}$
222		eldifsn	$⊢ t \in ((0 \dots N) ∖ \{z\}) \leftrightarrow (t \in (0 \dots N) \land t \neq z)$
223		undif	$⊢ \{t\} \subseteq (0 \dots N) ∖ \{z\} \leftrightarrow \{t\} \cup (((0 \dots N) ∖ \{z\}) ∖ \{t\}) = (0 \dots N) ∖ \{z\}$
224	221 222 223	3imtr3i	$⊢ (t \in (0 \dots N) \land t \neq z) \to \{t\} \cup (((0 \dots N) ∖ \{z\}) ∖ \{t\}) = (0 \dots N) ∖ \{z\}$
225	220 224	syl5eq	$⊢ (t \in (0 \dots N) \land t \neq z) \to \{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\}) = (0 \dots N) ∖ \{z\}$
226	218 225	sylan2	$⊢ (t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \to \{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\}) = (0 \dots N) ∖ \{z\}$
227	226	rexeqdv	$⊢ (t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \to (\exists j \in (\{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
228	227	adantr	$⊢ ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to (\exists j \in (\{t\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
229		snssi	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to \{z\} \subseteq (0 \dots N) ∖ \{t\}$
230		undif	$⊢ \{z\} \subseteq (0 \dots N) ∖ \{t\} \leftrightarrow \{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\}) = (0 \dots N) ∖ \{t\}$
231	229 230	sylib	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to \{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\}) = (0 \dots N) ∖ \{t\}$
232	231	rexeqdv	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to (\exists j \in (\{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
233	232	ad2antlr	$⊢ ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to (\exists j \in (\{z\} \cup (((0 \dots N) ∖ \{t\}) ∖ \{z\})) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
234	216 228 233	3bitr3d	$⊢ ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to (\exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
235	234	ralbidv	$⊢ ((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
236	235	biimpar	$⊢ (((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
237	236	an32s	$⊢ (((t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
238	198 237	sylan	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
239		simpl	$⊢ (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to t \in (0 \dots N)$
240	239	anim2i	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to (φ \land t \in (0 \dots N))$
241		necom	$⊢ z \neq t \leftrightarrow t \neq z$
242	241	biimpi	$⊢ z \neq t \to t \neq z$
243	242	adantl	$⊢ (z \in (0 \dots N) \land z \neq t) \to t \neq z$
244	243	anim2i	$⊢ (t \in (0 \dots N) \land (z \in (0 \dots N) \land z \neq t)) \to (t \in (0 \dots N) \land t \neq z)$
245		eldifsn	$⊢ z \in ((0 \dots N) ∖ \{t\}) \leftrightarrow (z \in (0 \dots N) \land z \neq t)$
246	245	anbi2i	$⊢ (t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \leftrightarrow (t \in (0 \dots N) \land (z \in (0 \dots N) \land z \neq t))$
247	244 246 222	3imtr4i	$⊢ (t \in (0 \dots N) \land z \in ((0 \dots N) ∖ \{t\})) \to t \in ((0 \dots N) ∖ \{z\})$
248	247	adantll	$⊢ ((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \to t \in ((0 \dots N) ∖ \{z\})$
249	248	adantr	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to t \in ((0 \dots N) ∖ \{z\})$
250	34	nfel1	$⊢ Ⅎ j ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
251	42 250	nfim	$⊢ Ⅎ j ((φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1))$
252	36	eleq1d	$⊢ j = t \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1))$
253	46 252	imbi12d	$⊢ j = t \to (((φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)) \leftrightarrow ((φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)))$
254	6	necomd	$⊢ (φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \neq N$
255	254	neneqd	$⊢ (φ \land j \in (0 \dots N)) \to \neg ⦋ ⟨T, U⟩ / s ⦌ C = N$
256		fzm1	$⊢ N \in ℤ_{\geq 0} \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ ⟨T, U⟩ / s ⦌ C = N))$
257	153 256	syl	$⊢ φ \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ ⟨T, U⟩ / s ⦌ C = N))$
258	257	adantr	$⊢ (φ \land j \in (0 \dots N)) \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N) \leftrightarrow (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ ⟨T, U⟩ / s ⦌ C = N))$
259	149 258	mpbid	$⊢ (φ \land j \in (0 \dots N)) \to (⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \lor ⦋ ⟨T, U⟩ / s ⦌ C = N)$
260	259	ord	$⊢ (φ \land j \in (0 \dots N)) \to (\neg ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \to ⦋ ⟨T, U⟩ / s ⦌ C = N)$
261	255 260	mt3d	$⊢ (φ \land j \in (0 \dots N)) \to ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
262	251 253 261	chvarfv	$⊢ (φ \land t \in (0 \dots N)) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
263	262	ad2antrr	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1)$
264		eldifi	$⊢ z \in ((0 \dots N) ∖ \{t\}) \to z \in (0 \dots N)$
265		eleq1w	$⊢ t = z \to (t \in (0 \dots N) \leftrightarrow z \in (0 \dots N))$
266	265	anbi2d	$⊢ t = z \to ((φ \land t \in (0 \dots N)) \leftrightarrow (φ \land z \in (0 \dots N)))$
267		sneq	$⊢ t = z \to \{t\} = \{z\}$
268	267	difeq2d	$⊢ t = z \to (0 \dots N) ∖ \{t\} = (0 \dots N) ∖ \{z\}$
269	268	breq2d	$⊢ t = z \to ((0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\}) \leftrightarrow (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\}))$
270	266 269	imbi12d	$⊢ t = z \to (((φ \land t \in (0 \dots N)) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{t\})) \leftrightarrow ((φ \land z \in (0 \dots N)) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\})))$
271	270 180	chvarvv	$⊢ (φ \land z \in (0 \dots N)) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\})$
272	264 271	sylan2	$⊢ (φ \land z \in ((0 \dots N) ∖ \{t\})) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\})$
273	272	adantlr	$⊢ ((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \to (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\})$
274		phpreu	$⊢ ((0 \dots N - 1) \in Fin \land (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\})) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
275	161 274	mpan	$⊢ (0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\}) \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
276	275	biimpa	$⊢ ((0 \dots N - 1) \approx ((0 \dots N) ∖ \{z\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
277	273 276	sylan	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
278		eqeq1	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
279	278	adantr	$⊢ (i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \land j \in ((0 \dots N) ∖ \{z\})) \to (i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
280	201 279	reubida	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
281	280	rspcv	$⊢ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \to (\forall i \in (0 \dots N - 1) \exists! j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists! j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
282	263 277 281	sylc	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists! j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
283		reurmo	$⊢ \exists! j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists^{*} j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
284	282 283	syl	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists^{*} j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
285		nfv	$⊢ Ⅎ i ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
286	285	rmo3	$⊢ \exists^{*} j \in ((0 \dots N) ∖ \{z\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall j \in ((0 \dots N) ∖ \{z\}) \forall i \in ((0 \dots N) ∖ \{z\}) ((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to j = i)$
287	284 286	sylib	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{z\}) \forall i \in ((0 \dots N) ∖ \{z\}) ((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to j = i)$
288		equcomi	$⊢ i = t \to t = i$
289	288	csbeq1d	$⊢ i = t \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
290		sbsbc	$⊢ [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \underset{˙}{[} i / j \underset{˙}{]} ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
291		vex	$⊢ i \in V$
292		sbceqg	$⊢ i \in V \to (\underset{˙}{[} i / j \underset{˙}{]} ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ i / j ⦌ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
293	34	csbconstgf	$⊢ i \in V \to ⦋ i / j ⦌ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
294	293	eqeq1d	$⊢ i \in V \to (⦋ i / j ⦌ ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
295	292 294	bitrd	$⊢ i \in V \to (\underset{˙}{[} i / j \underset{˙}{]} ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
296	291 295	ax-mp	$⊢ \underset{˙}{[} i / j \underset{˙}{]} ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
297	290 296	bitri	$⊢ [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ i / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
298	289 297	sylibr	$⊢ i = t \to [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
299	298	biantrud	$⊢ i = t \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
300	299	bicomd	$⊢ i = t \to ((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
301		eqeq2	$⊢ i = t \to (j = i \leftrightarrow j = t)$
302	300 301	imbi12d	$⊢ i = t \to (((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to j = i) \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t))$
303	302	rspcv	$⊢ t \in ((0 \dots N) ∖ \{z\}) \to (\forall i \in ((0 \dots N) ∖ \{z\}) ((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to j = i) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t))$
304	303	ralimdv	$⊢ t \in ((0 \dots N) ∖ \{z\}) \to (\forall j \in ((0 \dots N) ∖ \{z\}) \forall i \in ((0 \dots N) ∖ \{z\}) ((⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \land [i/ j] ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to j = i) \to \forall j \in ((0 \dots N) ∖ \{z\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t))$
305	249 287 304	sylc	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{z\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t)$
306		dif32	$⊢ ((0 \dots N) ∖ \{z\}) ∖ \{t\} = ((0 \dots N) ∖ \{t\}) ∖ \{z\}$
307	306	eleq2i	$⊢ j \in (((0 \dots N) ∖ \{z\}) ∖ \{t\}) \leftrightarrow j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\})$
308		eldifsn	$⊢ j \in (((0 \dots N) ∖ \{z\}) ∖ \{t\}) \leftrightarrow (j \in ((0 \dots N) ∖ \{z\}) \land j \neq t)$
309		eldifsn	$⊢ j \in (((0 \dots N) ∖ \{t\}) ∖ \{z\}) \leftrightarrow (j \in ((0 \dots N) ∖ \{t\}) \land j \neq z)$
310	307 308 309	3bitr3ri	$⊢ (j \in ((0 \dots N) ∖ \{t\}) \land j \neq z) \leftrightarrow (j \in ((0 \dots N) ∖ \{z\}) \land j \neq t)$
311	310	imbi1i	$⊢ ((j \in ((0 \dots N) ∖ \{t\}) \land j \neq z) \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow ((j \in ((0 \dots N) ∖ \{z\}) \land j \neq t) \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
312		impexp	$⊢ ((j \in ((0 \dots N) ∖ \{t\}) \land j \neq z) \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (j \in ((0 \dots N) ∖ \{t\}) \to (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
313		impexp	$⊢ ((j \in ((0 \dots N) ∖ \{z\}) \land j \neq t) \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (j \in ((0 \dots N) ∖ \{z\}) \to (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
314	311 312 313	3bitr3ri	$⊢ (j \in ((0 \dots N) ∖ \{z\}) \to (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)) \leftrightarrow (j \in ((0 \dots N) ∖ \{t\}) \to (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
315	314	albii	$⊢ \forall j (j \in ((0 \dots N) ∖ \{z\}) \to (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)) \leftrightarrow \forall j (j \in ((0 \dots N) ∖ \{t\}) \to (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
316		con34b	$⊢ (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t) \leftrightarrow (\neg j = t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
317		df-ne	$⊢ j \neq t \leftrightarrow \neg j = t$
318	317	imbi1i	$⊢ (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (\neg j = t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
319	316 318	bitr4i	$⊢ (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t) \leftrightarrow (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
320	319	ralbii	$⊢ \forall j \in ((0 \dots N) ∖ \{z\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t) \leftrightarrow \forall j \in ((0 \dots N) ∖ \{z\}) (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
321		df-ral	$⊢ \forall j \in ((0 \dots N) ∖ \{z\}) (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow \forall j (j \in ((0 \dots N) ∖ \{z\}) \to (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
322	320 321	bitri	$⊢ \forall j \in ((0 \dots N) ∖ \{z\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t) \leftrightarrow \forall j (j \in ((0 \dots N) ∖ \{z\}) \to (j \neq t \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
323		df-ral	$⊢ \forall j \in ((0 \dots N) ∖ \{t\}) (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow \forall j (j \in ((0 \dots N) ∖ \{t\}) \to (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
324	315 322 323	3bitr4i	$⊢ \forall j \in ((0 \dots N) ∖ \{z\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = t) \leftrightarrow \forall j \in ((0 \dots N) ∖ \{t\}) (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
325	305 324	sylib	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{t\}) (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
326		df-ne	$⊢ j \neq z \leftrightarrow \neg j = z$
327	326	imbi1i	$⊢ (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (\neg j = z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
328		con34b	$⊢ (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = z) \leftrightarrow (\neg j = z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
329	327 328	bitr4i	$⊢ (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = z)$
330		ancr	$⊢ (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to j = z) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
331	329 330	sylbi	$⊢ (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
332	331	ralimi	$⊢ \forall j \in ((0 \dots N) ∖ \{t\}) (j \neq z \to \neg ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{t\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
333	325 332	syl	$⊢ (((φ \land t \in (0 \dots N)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{t\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
334	240 333	sylanl1	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \forall j \in ((0 \dots N) ∖ \{t\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
335	201 278	rexbid	$⊢ i = ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \to (\exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
336	335	rspcva	$⊢ (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \in (0 \dots N - 1) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
337	262 336	sylan	$⊢ ((φ \land t \in (0 \dots N)) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
338	337	anasss	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to \exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
339	338	ad2antrr	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C$
340		rexim	$⊢ \forall j \in ((0 \dots N) ∖ \{t\}) (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)) \to (\exists j \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \to \exists j \in ((0 \dots N) ∖ \{t\}) (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C))$
341	334 339 340	sylc	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j \in ((0 \dots N) ∖ \{t\}) (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
342		rexex	$⊢ \exists j \in ((0 \dots N) ∖ \{t\}) (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
343	341 342	syl	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to \exists j (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C)$
344	34 186	nfeq	$⊢ Ⅎ j ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
345	188	eqeq2d	$⊢ j = z \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C)$
346	344 345	equsexv	$⊢ \exists j (j = z \land ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
347	343 346	sylib	$⊢ (((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \to ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C$
348	238 347	impbida	$⊢ ((φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \land z \in ((0 \dots N) ∖ \{t\})) \to (⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
349	348	reubidva	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to (\exists! z \in ((0 \dots N) ∖ \{t\}) ⦋ t / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C = ⦋ z / j ⦌ ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! z \in ((0 \dots N) ∖ \{t\}) \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
350	195 349	mpbid	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to \exists! z \in ((0 \dots N) ∖ \{t\}) \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C$
351		an32	$⊢ ((z \in (0 \dots N) \land z \neq t) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow ((z \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \land z \neq t)$
352	245	anbi1i	$⊢ (z \in ((0 \dots N) ∖ \{t\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow ((z \in (0 \dots N) \land z \neq t) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
353		sneq	$⊢ y = z \to \{y\} = \{z\}$
354	353	difeq2d	$⊢ y = z \to (0 \dots N) ∖ \{y\} = (0 \dots N) ∖ \{z\}$
355	354	rexeqdv	$⊢ y = z \to (\exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
356	355	ralbidv	$⊢ y = z \to (\forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
357	356	elrab	$⊢ z \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \leftrightarrow (z \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
358	357	anbi1i	$⊢ (z \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \land z \neq t) \leftrightarrow ((z \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \land z \neq t)$
359	351 352 358	3bitr4i	$⊢ (z \in ((0 \dots N) ∖ \{t\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow (z \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \land z \neq t)$
360		eldifsn	$⊢ z \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}) \leftrightarrow (z \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \land z \neq t)$
361	359 360	bitr4i	$⊢ (z \in ((0 \dots N) ∖ \{t\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow z \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\})$
362	361	eubii	$⊢ \exists! z (z \in ((0 \dots N) ∖ \{t\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C) \leftrightarrow \exists! z z \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\})$
363		df-reu	$⊢ \exists! z \in ((0 \dots N) ∖ \{t\}) \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \exists! z (z \in ((0 \dots N) ∖ \{t\}) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)$
364		euhash1	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\} \in Fin \to (\|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| = 1 \leftrightarrow \exists! z z \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}))$
365	18 364	ax-mp	$⊢ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| = 1 \leftrightarrow \exists! z z \in (\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\})$
366	362 363 365	3bitr4i	$⊢ \exists! z \in ((0 \dots N) ∖ \{t\}) \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{z\}) i = ⦋ ⟨T, U⟩ / s ⦌ C \leftrightarrow \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| = 1$
367	350 366	sylib	$⊢ (φ \land (t \in (0 \dots N) \land \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{t\}) i = ⦋ ⟨T, U⟩ / s ⦌ C)) \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| = 1$
368	31 367	sylan2b	$⊢ (φ \land t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}) \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| = 1$
369	368	oveq1d	$⊢ (φ \land t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}) \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} ∖ \{t\}\| + 1 = 1 + 1$
370	26 369	eqtr3d	$⊢ (φ \land t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}) \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\| = 1 + 1$
371	12 370	breqtrrid	$⊢ (φ \land t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}) \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$
372	371	ex	$⊢ φ \to (t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|)$
373	372	exlimdv	$⊢ φ \to (\exists t t \in \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|)$
374	7 373	syl5bi	$⊢ φ \to (\neg \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} = \emptyset \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|)$
375		dvds0	$⊢ 2 \in ℤ \to 2 ∥ 0$
376	8 375	ax-mp	$⊢ 2 ∥ 0$
377		hash0	$⊢ \|\emptyset\| = 0$
378	376 377	breqtrri	$⊢ 2 ∥ \|\emptyset\|$
379		fveq2	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} = \emptyset \to \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\| = \|\emptyset\|$
380	378 379	breqtrrid	$⊢ \{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\} = \emptyset \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$
381	374 380	pm2.61d2	$⊢ φ \to 2 ∥ \|\{y \in (0 \dots N) \| \forall i \in (0 \dots N - 1) \exists j \in ((0 \dots N) ∖ \{y\}) i = ⦋ ⟨T, U⟩ / s ⦌ C\}\|$

Metamath Proof Explorer

Theorem poimirlem25

Proof