poimirlem9

Description: Lemma for poimir , establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem9.1	$⊢ φ \to T \in S$
	poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
	poimirlem9.3	$⊢ φ \to U \in S$
	poimirlem9.4	$⊢ φ \to 2^{nd} (1^{st} (U)) \neq 2^{nd} (1^{st} (T))$
Assertion	poimirlem9	$⊢ φ \to 2^{nd} (1^{st} (U)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem9.1	$⊢ φ \to T \in S$
4		poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
5		poimirlem9.3	$⊢ φ \to U \in S$
6		poimirlem9.4	$⊢ φ \to 2^{nd} (1^{st} (U)) \neq 2^{nd} (1^{st} (T))$
7		resundi	$⊢ {2^{nd} (1^{st} (U)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
8	1	nncnd	$⊢ φ \to N \in ℂ$
9		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
10	8 9	syl	$⊢ φ \to N - 1 + 1 = N$
11	1	nnzd	$⊢ φ \to N \in ℤ$
12		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
13		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
14		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
15	11 12 13 14	4syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
16	10 15	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
17		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
18	16 17	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
19	18 4	sseldd	$⊢ φ \to 2^{nd} (T) \in (1 \dots N)$
20		fzp1elp1	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
21	4 20	syl	$⊢ φ \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
22	10	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
23	21 22	eleqtrd	$⊢ φ \to 2^{nd} (T) + 1 \in (1 \dots N)$
24	19 23	prssd	$⊢ φ \to \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)$
25		undif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) \leftrightarrow \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N)$
26	24 25	sylib	$⊢ φ \to \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots N)$
27	26	reseq2d	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = {2^{nd} (1^{st} (U)) ↾}_{(1 \dots N)}$
28		elrabi	$⊢ U \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
29	28 2	eleq2s	$⊢ U \in S \to U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
30		xp1st	$⊢ U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
31		xp2nd	$⊢ 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
32	5 29 30 31	4syl	$⊢ φ \to 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
33		fvex	$⊢ 2^{nd} (1^{st} (U)) \in V$
34		f1oeq1	$⊢ f = 2^{nd} (1^{st} (U)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
35	33 34	elab	$⊢ 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
36	32 35	sylib	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
37		f1ofn	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) Fn (1 \dots N)$
38		fnresdm	$⊢ 2^{nd} (1^{st} (U)) Fn (1 \dots N) \to {2^{nd} (1^{st} (U)) ↾}_{(1 \dots N)} = 2^{nd} (1^{st} (U))$
39	36 37 38	3syl	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{(1 \dots N)} = 2^{nd} (1^{st} (U))$
40	27 39	eqtrd	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = 2^{nd} (1^{st} (U))$
41	7 40	eqtr3id	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = 2^{nd} (1^{st} (U))$
42		2lt3	$⊢ 2 < 3$
43		2re	$⊢ 2 \in ℝ$
44		3re	$⊢ 3 \in ℝ$
45	43 44	ltnlei	$⊢ 2 < 3 \leftrightarrow \neg 3 \leq 2$
46	42 45	mpbi	$⊢ \neg 3 \leq 2$
47		df-pr	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} \cup \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
48	47	coeq2i	$⊢ 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} \cup \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
49		coundi	$⊢ 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} \cup \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) = (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
50	48 49	eqtri	$⊢ 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
51		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
52	51 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
53		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
54		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
55	3 52 53 54	4syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
56		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
57		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
58	56 57	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
59	55 58	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
60		f1of1	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
61	59 60	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
62	23	snssd	$⊢ φ \to \{2^{nd} (T) + 1\} \subseteq (1 \dots N)$
63		f1ores	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land \{2^{nd} (T) + 1\} \subseteq (1 \dots N)) \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
64	61 62 63	syl2anc	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
65		f1of	$⊢ ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}] \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
66	64 65	syl	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
67		f1ofn	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
68	59 67	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
69		fnsnfv	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N)) \to \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} = 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
70	68 23 69	syl2anc	$⊢ φ \to \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} = 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}]$
71	70	feq3d	$⊢ φ \to (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} \leftrightarrow ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1\}])$
72	66 71	mpbird	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
73		eqid	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}$
74		fvex	$⊢ 2^{nd} (T) \in V$
75		ovex	$⊢ 2^{nd} (T) + 1 \in V$
76	74 75	fsn	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} : \{2^{nd} (T)\} ⟶ \{2^{nd} (T) + 1\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}$
77	73 76	mpbir	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} : \{2^{nd} (T)\} ⟶ \{2^{nd} (T) + 1\}$
78		fco2	$⊢ (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) : \{2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} \land \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} : \{2^{nd} (T)\} ⟶ \{2^{nd} (T) + 1\}) \to (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) : \{2^{nd} (T)\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
79	72 77 78	sylancl	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) : \{2^{nd} (T)\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
80		fvex	$⊢ 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \in V$
81	80	fconst2	$⊢ (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) : \{2^{nd} (T)\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} \leftrightarrow 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} = \{2^{nd} (T)\} \times \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
82	79 81	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} = \{2^{nd} (T)\} \times \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
83	74 80	xpsn	$⊢ \{2^{nd} (T)\} \times \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
84	82 83	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
85	84	uneq1d	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩\}) \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
86	50 85	syl5eq	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
87		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
88	4 87	syl	$⊢ φ \to 2^{nd} (T) \in ℕ$
89	88	nnred	$⊢ φ \to 2^{nd} (T) \in ℝ$
90	89	ltp1d	$⊢ φ \to 2^{nd} (T) < 2^{nd} (T) + 1$
91	89 90	ltned	$⊢ φ \to 2^{nd} (T) \neq 2^{nd} (T) + 1$
92	91	necomd	$⊢ φ \to 2^{nd} (T) + 1 \neq 2^{nd} (T)$
93		f1veqaeq	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land (2^{nd} (T) + 1 \in (1 \dots N) \land 2^{nd} (T) \in (1 \dots N))) \to (2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) = 2^{nd} (1^{st} (T)) (2^{nd} (T)) \to 2^{nd} (T) + 1 = 2^{nd} (T))$
94	61 23 19 93	syl12anc	$⊢ φ \to (2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) = 2^{nd} (1^{st} (T)) (2^{nd} (T)) \to 2^{nd} (T) + 1 = 2^{nd} (T))$
95	94	necon3d	$⊢ φ \to (2^{nd} (T) + 1 \neq 2^{nd} (T) \to 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T)))$
96	92 95	mpd	$⊢ φ \to 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T))$
97	96	neneqd	$⊢ φ \to \neg 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) = 2^{nd} (1^{st} (T)) (2^{nd} (T))$
98	74 80	opth	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \leftrightarrow (2^{nd} (T) = 2^{nd} (T) \land 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) = 2^{nd} (1^{st} (T)) (2^{nd} (T)))$
99	98	simprbi	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \to 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) = 2^{nd} (1^{st} (T)) (2^{nd} (T))$
100	97 99	nsyl	$⊢ φ \to \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩$
101	91	neneqd	$⊢ φ \to \neg 2^{nd} (T) = 2^{nd} (T) + 1$
102	74 80	opth1	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \to 2^{nd} (T) = 2^{nd} (T) + 1$
103	101 102	nsyl	$⊢ φ \to \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩$
104		opex	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in V$
105	104	snid	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
106		elun1	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \to ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in (\{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}))$
107	105 106	ax-mp	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in (\{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}))$
108		eleq2	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \to (⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in (\{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})) \leftrightarrow ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\})$
109	107 108	mpbii	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \to ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
110	104	elpr	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \leftrightarrow (⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \lor ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩)$
111		oran	$⊢ (⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \lor ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩) \leftrightarrow \neg (\neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \land \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩)$
112	110 111	bitri	$⊢ ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ \in \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \leftrightarrow \neg (\neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \land \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩)$
113	109 112	sylib	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \to \neg (\neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \land \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩)$
114	113	necon2ai	$⊢ (\neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩ \land \neg ⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩ = ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩) \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
115	100 103 114	syl2anc	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \cup (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
116	86 115	eqnetrd	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
117		fnressn	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 2^{nd} (T) \in (1 \dots N)) \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T)\}} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩\}$
118	68 19 117	syl2anc	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T)\}} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩\}$
119		fnressn	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N)) \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}} = \{⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
120	68 23 119	syl2anc	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}} = \{⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
121	118 120	uneq12d	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T)\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}}) = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩\} \cup \{⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
122		df-pr	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} = \{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}$
123	122	reseq2i	$⊢ {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = {2^{nd} (1^{st} (T)) ↾}_{(\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})}$
124		resundi	$⊢ {2^{nd} (1^{st} (T)) ↾}_{(\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})} = ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T)\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}})$
125	123 124	eqtri	$⊢ {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T)\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1\}})$
126		df-pr	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩\} \cup \{⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
127	121 125 126	3eqtr4g	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}$
128	1 2 3 4 5	poimirlem8	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}$
129		uneq12	$⊢ ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \land {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
130		resundi	$⊢ {2^{nd} (1^{st} (T)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
131	26	reseq2d	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = {2^{nd} (1^{st} (T)) ↾}_{(1 \dots N)}$
132		fnresdm	$⊢ 2^{nd} (1^{st} (T)) Fn (1 \dots N) \to {2^{nd} (1^{st} (T)) ↾}_{(1 \dots N)} = 2^{nd} (1^{st} (T))$
133	59 67 132	3syl	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{(1 \dots N)} = 2^{nd} (1^{st} (T))$
134	131 133	eqtrd	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{(\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))} = 2^{nd} (1^{st} (T))$
135	130 134	eqtr3id	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = 2^{nd} (1^{st} (T))$
136	41 135	eqeq12d	$⊢ φ \to (({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) \leftrightarrow 2^{nd} (1^{st} (U)) = 2^{nd} (1^{st} (T)))$
137	129 136	syl5ib	$⊢ φ \to (({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \land {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) \to 2^{nd} (1^{st} (U)) = 2^{nd} (1^{st} (T)))$
138	128 137	mpan2d	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \to 2^{nd} (1^{st} (U)) = 2^{nd} (1^{st} (T)))$
139	138	necon3d	$⊢ φ \to (2^{nd} (1^{st} (U)) \neq 2^{nd} (1^{st} (T)) \to {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}})$
140	6 139	mpd	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}$
141	140	necomd	$⊢ φ \to {2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}$
142	127 141	eqnetrrd	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}$
143		prex	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \in V$
144	56 143	coex	$⊢ 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \in V$
145		prex	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \in V$
146	33	resex	$⊢ {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in V$
147		hashtpg	$⊢ (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \in V \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \in V \land {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in V) \to ((2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \land {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \leftrightarrow \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3)$
148	144 145 146 147	mp3an	$⊢ (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \land {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \leftrightarrow \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3$
149	148	biimpi	$⊢ (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \land {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3$
150	149	3expia	$⊢ (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \neq \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \neq {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3)$
151	116 142 150	syl2anc	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3)$
152		prex	$⊢ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \in V$
153		prex	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \in V$
154	152 153	mapval	$⊢ {\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} = \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}$
155		prfi	$⊢ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \in Fin$
156		prfi	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin$
157		mapfi	$⊢ (\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \in Fin \land \{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin) \to {\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in Fin$
158	155 156 157	mp2an	$⊢ {\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in Fin$
159	154 158	eqeltrri	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin$
160		f1of	$⊢ f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \to f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
161	160	ss2abi	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}$
162		ssfi	$⊢ (\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin \land \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}) \to \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin$
163	159 161 162	mp2an	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin$
164	23 19	prssd	$⊢ φ \to \{2^{nd} (T) + 1, 2^{nd} (T)\} \subseteq (1 \dots N)$
165		f1ores	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land \{2^{nd} (T) + 1, 2^{nd} (T)\} \subseteq (1 \dots N)) \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1, 2^{nd} (T)\}]$
166	61 164 165	syl2anc	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1, 2^{nd} (T)\}]$
167		fnimapr	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N) \land 2^{nd} (T) \in (1 \dots N)) \to 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1, 2^{nd} (T)\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
168	68 23 19 167	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1, 2^{nd} (T)\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
169	168	f1oeq3d	$⊢ φ \to (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (T)) [\{2^{nd} (T) + 1, 2^{nd} (T)\}] \leftrightarrow ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
170	166 169	mpbid	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
171		f1oprg	$⊢ ((2^{nd} (T) \in V \land 2^{nd} (T) + 1 \in V) \land (2^{nd} (T) + 1 \in V \land 2^{nd} (T) \in V)) \to ((2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \neq 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\})$
172	74 75 75 74 171	mp4an	$⊢ (2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (T) + 1 \neq 2^{nd} (T)) \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}$
173	91 92 172	syl2anc	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}$
174		f1oco	$⊢ (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) : \{2^{nd} (T) + 1, 2^{nd} (T)\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \land \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T) + 1, 2^{nd} (T)\}) \to (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
175	170 173 174	syl2anc	$⊢ φ \to (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
176		rnpropg	$⊢ (2^{nd} (T) \in V \land 2^{nd} (T) + 1 \in V) \to ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T) + 1, 2^{nd} (T)\}$
177	74 75 176	mp2an	$⊢ ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = \{2^{nd} (T) + 1, 2^{nd} (T)\}$
178	177	eqimssi	$⊢ ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \subseteq \{2^{nd} (T) + 1, 2^{nd} (T)\}$
179		cores	$⊢ ran \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \subseteq \{2^{nd} (T) + 1, 2^{nd} (T)\} \to ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
180		f1oeq1	$⊢ ({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} = 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \to ((({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
181	178 179 180	mp2b	$⊢ (({2^{nd} (1^{st} (T)) ↾}_{\{2^{nd} (T) + 1, 2^{nd} (T)\}}) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
182	175 181	sylib	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
183	96	necomd	$⊢ φ \to 2^{nd} (1^{st} (T)) (2^{nd} (T)) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)$
184		fvex	$⊢ 2^{nd} (1^{st} (T)) (2^{nd} (T)) \in V$
185		f1oprg	$⊢ ((2^{nd} (T) \in V \land 2^{nd} (1^{st} (T)) (2^{nd} (T)) \in V) \land (2^{nd} (T) + 1 \in V \land 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \in V)) \to ((2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (1^{st} (T)) (2^{nd} (T)) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)) \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\})$
186	74 184 75 80 185	mp4an	$⊢ (2^{nd} (T) \neq 2^{nd} (T) + 1 \land 2^{nd} (1^{st} (T)) (2^{nd} (T)) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)) \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
187	91 183 186	syl2anc	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
188		prcom	$⊢ \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
189		f1oeq3	$⊢ \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \to (\{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
190	188 189	ax-mp	$⊢ \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
191	187 190	sylib	$⊢ φ \to \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
192		f1of1	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
193	36 192	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
194		f1ores	$⊢ (2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)) \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (U)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
195	193 24 194	syl2anc	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (U)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
196		dff1o3	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (U)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (U))}^{-1})$
197	196	simprbi	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (U))}^{-1}$
198		imadif	$⊢ Fun {2^{nd} (1^{st} (U))}^{-1} \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
199	36 197 198	3syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
200		f1ofo	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
201		foima	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = (1 \dots N)$
202	36 200 201	3syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = (1 \dots N)$
203		f1ofo	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
204		foima	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
205	59 203 204	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
206	202 205	eqtr4d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots N)]$
207	128	rneqd	$⊢ φ \to ran ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = ran ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
208		df-ima	$⊢ 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = ran ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
209		df-ima	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = ran ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
210	207 208 209	3eqtr4g	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
211	206 210	difeq12d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
212		dff1o3	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (T))}^{-1})$
213	212	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
214		imadif	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
215	59 213 214	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}]$
216		dfin4	$⊢ (1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
217		sseqin2	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N) \leftrightarrow (1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
218	24 217	sylib	$⊢ φ \to (1 \dots N) \cap \{2^{nd} (T), 2^{nd} (T) + 1\} = \{2^{nd} (T), 2^{nd} (T) + 1\}$
219	216 218	eqtr3id	$⊢ φ \to (1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \{2^{nd} (T), 2^{nd} (T) + 1\}$
220	219	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
221	215 220	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}] = 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
222	199 211 221	3eqtrd	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
223	219	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})] = 2^{nd} (1^{st} (U)) [\{2^{nd} (T), 2^{nd} (T) + 1\}]$
224		fnimapr	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 2^{nd} (T) \in (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N)) \to 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
225	68 19 23 224	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T)), 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)\}$
226	225 188	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
227	222 223 226	3eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [\{2^{nd} (T), 2^{nd} (T) + 1\}] = \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
228	227	f1oeq3d	$⊢ φ \to (({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} 2^{nd} (1^{st} (U)) [\{2^{nd} (T), 2^{nd} (T) + 1\}] \leftrightarrow ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
229	195 228	mpbid	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
230		ssabral	$⊢ \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \leftrightarrow \forall f \in \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}$
231		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \to (f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
232		f1oeq1	$⊢ f = \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} \to (f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
233		f1oeq1	$⊢ f = {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \to (f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
234	144 145 146 231 232 233	raltp	$⊢ \forall f \in \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \leftrightarrow ((2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \land ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
235	230 234	bitri	$⊢ \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \leftrightarrow ((2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \land \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \land ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\})$
236	182 191 229 235	syl3anbrc	$⊢ φ \to \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}$
237		hashss	$⊢ (\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin \land \{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}) \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| \leq \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\|$
238	163 236 237	sylancr	$⊢ φ \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| \leq \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\|$
239	153	enref	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\}$
240		hashprg	$⊢ (2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \in V \land 2^{nd} (1^{st} (T)) (2^{nd} (T)) \in V) \to (2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T)) \leftrightarrow \|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = 2)$
241	80 184 240	mp2an	$⊢ 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \neq 2^{nd} (1^{st} (T)) (2^{nd} (T)) \leftrightarrow \|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = 2$
242	96 241	sylib	$⊢ φ \to \|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = 2$
243		hashprg	$⊢ (2^{nd} (T) \in V \land 2^{nd} (T) + 1 \in V) \to (2^{nd} (T) \neq 2^{nd} (T) + 1 \leftrightarrow \|\{2^{nd} (T), 2^{nd} (T) + 1\}\| = 2)$
244	74 75 243	mp2an	$⊢ 2^{nd} (T) \neq 2^{nd} (T) + 1 \leftrightarrow \|\{2^{nd} (T), 2^{nd} (T) + 1\}\| = 2$
245	91 244	sylib	$⊢ φ \to \|\{2^{nd} (T), 2^{nd} (T) + 1\}\| = 2$
246	242 245	eqtr4d	$⊢ φ \to \|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = \|\{2^{nd} (T), 2^{nd} (T) + 1\}\|$
247		hashen	$⊢ (\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \in Fin \land \{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin) \to (\|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = \|\{2^{nd} (T), 2^{nd} (T) + 1\}\| \leftrightarrow \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\})$
248	155 156 247	mp2an	$⊢ \|\{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\| = \|\{2^{nd} (T), 2^{nd} (T) + 1\}\| \leftrightarrow \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\}$
249	246 248	sylib	$⊢ φ \to \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\}$
250		hashfacen	$⊢ (\{2^{nd} (T), 2^{nd} (T) + 1\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\} \land \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\} \approx \{2^{nd} (T), 2^{nd} (T) + 1\}) \to \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \approx \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}$
251	239 249 250	sylancr	$⊢ φ \to \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \approx \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}$
252	153 153	mapval	$⊢ {\{2^{nd} (T), 2^{nd} (T) + 1\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} = \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}\}$
253		mapfi	$⊢ (\{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin \land \{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin) \to {\{2^{nd} (T), 2^{nd} (T) + 1\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in Fin$
254	156 156 253	mp2an	$⊢ {\{2^{nd} (T), 2^{nd} (T) + 1\}}^{\{2^{nd} (T), 2^{nd} (T) + 1\}} \in Fin$
255	252 254	eqeltrri	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}\} \in Fin$
256		f1of	$⊢ f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\} \to f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}$
257	256	ss2abi	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}\}$
258		ssfi	$⊢ (\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}\} \in Fin \land \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\} \subseteq \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T), 2^{nd} (T) + 1\}\}) \to \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\} \in Fin$
259	255 257 258	mp2an	$⊢ \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\} \in Fin$
260		hashen	$⊢ (\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \in Fin \land \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\} \in Fin) \to (\|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\| = \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\| \leftrightarrow \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \approx \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\})$
261	163 259 260	mp2an	$⊢ \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\| = \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\| \leftrightarrow \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\} \approx \{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}$
262	251 261	sylibr	$⊢ φ \to \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\| = \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\|$
263		hashfac	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \in Fin \to \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\| = \|\{2^{nd} (T), 2^{nd} (T) + 1\}\|!$
264	156 263	ax-mp	$⊢ \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\| = \|\{2^{nd} (T), 2^{nd} (T) + 1\}\|!$
265	245	fveq2d	$⊢ φ \to \|\{2^{nd} (T), 2^{nd} (T) + 1\}\|! = 2!$
266		fac2	$⊢ 2! = 2$
267	265 266	eqtrdi	$⊢ φ \to \|\{2^{nd} (T), 2^{nd} (T) + 1\}\|! = 2$
268	264 267	syl5eq	$⊢ φ \to \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (T), 2^{nd} (T) + 1\}\}\| = 2$
269	262 268	eqtrd	$⊢ φ \to \|\{f \| f : \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} \{2^{nd} (1^{st} (T)) (2^{nd} (T) + 1), 2^{nd} (1^{st} (T)) (2^{nd} (T))\}\}\| = 2$
270	238 269	breqtrd	$⊢ φ \to \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| \leq 2$
271		breq1	$⊢ \|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3 \to (\|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| \leq 2 \leftrightarrow 3 \leq 2)$
272	270 271	syl5ibcom	$⊢ φ \to (\|\{2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}, \{⟨2^{nd} (T), 2^{nd} (1^{st} (T)) (2^{nd} (T))⟩, ⟨2^{nd} (T) + 1, 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)⟩\}, {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}\}\| = 3 \to 3 \leq 2)$
273	151 272	syld	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} \neq 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \to 3 \leq 2)$
274	273	necon1bd	$⊢ φ \to (\neg 3 \leq 2 \to {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\})$
275	46 274	mpi	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}} = 2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}$
276		coires1	$⊢ 2^{nd} (1^{st} (T)) \circ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}$
277	128 276	eqtr4di	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = 2^{nd} (1^{st} (T)) \circ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})$
278	275 277	uneq12d	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{\{2^{nd} (T), 2^{nd} (T) + 1\}}) \cup ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) = (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \cup (2^{nd} (1^{st} (T)) \circ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
279	41 278	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) = (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \cup (2^{nd} (1^{st} (T)) \circ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
280		coundi	$⊢ 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) = (2^{nd} (1^{st} (T)) \circ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\}) \cup (2^{nd} (1^{st} (T)) \circ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
281	279 280	eqtr4di	$⊢ φ \to 2^{nd} (1^{st} (U)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$

Metamath Proof Explorer

Theorem poimirlem9

Proof