poimirlem12

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (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\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
	poimirlem12.2	$⊢ φ \to T \in S$
	poimirlem12.3	$⊢ φ \to 2^{nd} (T) = N$
	poimirlem12.4	$⊢ φ \to U \in S$
	poimirlem12.5	$⊢ φ \to 2^{nd} (U) = N$
	poimirlem12.6	$⊢ φ \to M \in (0 \dots N - 1)$
Assertion	poimirlem12	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots M)]$

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		poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
4		poimirlem12.2	$⊢ φ \to T \in S$
5		poimirlem12.3	$⊢ φ \to 2^{nd} (T) = N$
6		poimirlem12.4	$⊢ φ \to U \in S$
7		poimirlem12.5	$⊢ φ \to 2^{nd} (U) = N$
8		poimirlem12.6	$⊢ φ \to M \in (0 \dots N - 1)$
9		eldif	$⊢ y \in (2^{nd} (1^{st} (T)) [(1 \dots M)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)]) \leftrightarrow (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])$
10		imassrn	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq ran 2^{nd} (1^{st} (T))$
11		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))$
12	11 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))$
13		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)\})$
14	4 12 13	3syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
15		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)\}$
16	14 15	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
17		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
18		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))$
19	17 18	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)$
20	16 19	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
21		f1of	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
22		frn	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N) \to ran 2^{nd} (1^{st} (T)) \subseteq (1 \dots N)$
23	20 21 22	3syl	$⊢ φ \to ran 2^{nd} (1^{st} (T)) \subseteq (1 \dots N)$
24	10 23	sstrid	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq (1 \dots N)$
25		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))$
26	25 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))$
27		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)\})$
28	6 26 27	3syl	$⊢ φ \to 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
29		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)\}$
30	28 29	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
31		fvex	$⊢ 2^{nd} (1^{st} (U)) \in V$
32		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))$
33	31 32	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)$
34	30 33	sylib	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
35		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)$
36		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)$
37	34 35 36	3syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = (1 \dots N)$
38	24 37	sseqtrrd	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots N)]$
39	38	ssdifd	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)]$
40		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})$
41	40	simprbi	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (U))}^{-1}$
42		imadif	$⊢ Fun {2^{nd} (1^{st} (U))}^{-1} \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ (1 \dots M)] = 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)]$
43	34 41 42	3syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ (1 \dots M)] = 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)]$
44		difun2	$⊢ ((M + 1 \dots N) \cup (1 \dots M)) ∖ (1 \dots M) = (M + 1 \dots N) ∖ (1 \dots M)$
45		elfznn0	$⊢ M \in (0 \dots N - 1) \to M \in ℕ_{0}$
46		nn0p1nn	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ$
47	8 45 46	3syl	$⊢ φ \to M + 1 \in ℕ$
48		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
49	47 48	eleqtrdi	$⊢ φ \to M + 1 \in ℤ_{\geq 1}$
50	1	nncnd	$⊢ φ \to N \in ℂ$
51		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
52	50 51	syl	$⊢ φ \to N - 1 + 1 = N$
53		elfzuz3	$⊢ M \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq M}$
54		peano2uz	$⊢ N - 1 \in ℤ_{\geq M} \to N - 1 + 1 \in ℤ_{\geq M}$
55	8 53 54	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq M}$
56	52 55	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq M}$
57		fzsplit2	$⊢ (M + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq M}) \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
58	49 56 57	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
59		uncom	$⊢ (1 \dots M) \cup (M + 1 \dots N) = (M + 1 \dots N) \cup (1 \dots M)$
60	58 59	eqtrdi	$⊢ φ \to (1 \dots N) = (M + 1 \dots N) \cup (1 \dots M)$
61	60	difeq1d	$⊢ φ \to (1 \dots N) ∖ (1 \dots M) = ((M + 1 \dots N) \cup (1 \dots M)) ∖ (1 \dots M)$
62		incom	$⊢ (M + 1 \dots N) \cap (1 \dots M) = (1 \dots M) \cap (M + 1 \dots N)$
63	8 45	syl	$⊢ φ \to M \in ℕ_{0}$
64	63	nn0red	$⊢ φ \to M \in ℝ$
65	64	ltp1d	$⊢ φ \to M < M + 1$
66		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
67	65 66	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
68	62 67	eqtrid	$⊢ φ \to (M + 1 \dots N) \cap (1 \dots M) = \emptyset$
69		disj3	$⊢ (M + 1 \dots N) \cap (1 \dots M) = \emptyset \leftrightarrow (M + 1 \dots N) = (M + 1 \dots N) ∖ (1 \dots M)$
70	68 69	sylib	$⊢ φ \to (M + 1 \dots N) = (M + 1 \dots N) ∖ (1 \dots M)$
71	44 61 70	3eqtr4a	$⊢ φ \to (1 \dots N) ∖ (1 \dots M) = (M + 1 \dots N)$
72	71	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ (1 \dots M)] = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
73	43 72	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)] = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
74	39 73	sseqtrd	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
75	74	sselda	$⊢ (φ \land y \in (2^{nd} (1^{st} (T)) [(1 \dots M)] ∖ 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
76	9 75	sylan2br	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
77		fveq2	$⊢ t = U \to 2^{nd} (t) = 2^{nd} (U)$
78	77	breq2d	$⊢ t = U \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (U))$
79	78	ifbid	$⊢ t = U \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (U), y, y + 1)$
80	79	csbeq1d	$⊢ t = U \to ⦋ 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\}))) = ⦋ if (y < 2^{nd} (U), 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\})))$
81		2fveq3	$⊢ t = U \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (U))$
82		2fveq3	$⊢ t = U \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (U))$
83	82	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (U)) [(1 \dots j)]$
84	83	xpeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}$
85	82	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(j + 1 \dots N)]$
86	85	xpeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}$
87	84 86	uneq12d	$⊢ t = U \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})$
88	81 87	oveq12d	$⊢ t = U \to 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\})) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))$
89	88	csbeq2dv	$⊢ t = U \to ⦋ if (y < 2^{nd} (U), 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\}))) = ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))$
90	80 89	eqtrd	$⊢ t = U \to ⦋ 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\}))) = ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))$
91	90	mpteq2dv	$⊢ t = U \to (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\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
92	91	eqeq2d	$⊢ t = U \to (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\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))))$
93	92 2	elrab2	$⊢ U \in S \leftrightarrow (U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))))$
94	93	simprbi	$⊢ U \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
95	6 94	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
96		breq1	$⊢ y = M \to (y < 2^{nd} (U) \leftrightarrow M < 2^{nd} (U))$
97		id	$⊢ y = M \to y = M$
98	96 97	ifbieq1d	$⊢ y = M \to if (y < 2^{nd} (U), y, y + 1) = if (M < 2^{nd} (U), M, y + 1)$
99	1	nnred	$⊢ φ \to N \in ℝ$
100		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
101	99 100	syl	$⊢ φ \to N - 1 \in ℝ$
102		elfzle2	$⊢ M \in (0 \dots N - 1) \to M \leq N - 1$
103	8 102	syl	$⊢ φ \to M \leq N - 1$
104	99	ltm1d	$⊢ φ \to N - 1 < N$
105	64 101 99 103 104	lelttrd	$⊢ φ \to M < N$
106	105 7	breqtrrd	$⊢ φ \to M < 2^{nd} (U)$
107	106	iftrued	$⊢ φ \to if (M < 2^{nd} (U), M, y + 1) = M$
108	98 107	sylan9eqr	$⊢ (φ \land y = M) \to if (y < 2^{nd} (U), y, y + 1) = M$
109	108	csbeq1d	$⊢ (φ \land y = M) \to ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ M / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))$
110		oveq2	$⊢ j = M \to (1 \dots j) = (1 \dots M)$
111	110	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(1 \dots j)] = 2^{nd} (1^{st} (U)) [(1 \dots M)]$
112	111	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}$
113		oveq1	$⊢ j = M \to j + 1 = M + 1$
114	113	oveq1d	$⊢ j = M \to (j + 1 \dots N) = (M + 1 \dots N)$
115	114	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
116	115	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}$
117	112 116	uneq12d	$⊢ j = M \to (2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})$
118	117	oveq2d	$⊢ j = M \to 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
119	118	adantl	$⊢ (φ \land j = M) \to 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
120	8 119	csbied	$⊢ φ \to ⦋ M / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
121	120	adantr	$⊢ (φ \land y = M) \to ⦋ M / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
122	109 121	eqtrd	$⊢ (φ \land y = M) \to ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
123		ovexd	$⊢ φ \to 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) \in V$
124	95 122 8 123	fvmptd	$⊢ φ \to F (M) = 1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))$
125	124	fveq1d	$⊢ φ \to F (M) (y) = (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))) (y)$
126	125	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to F (M) (y) = (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))) (y)$
127		imassrn	$⊢ 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \subseteq ran 2^{nd} (1^{st} (U))$
128		f1of	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) : (1 \dots N) ⟶ (1 \dots N)$
129		frn	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) ⟶ (1 \dots N) \to ran 2^{nd} (1^{st} (U)) \subseteq (1 \dots N)$
130	34 128 129	3syl	$⊢ φ \to ran 2^{nd} (1^{st} (U)) \subseteq (1 \dots N)$
131	127 130	sstrid	$⊢ φ \to 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \subseteq (1 \dots N)$
132	131	sselda	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to y \in (1 \dots N)$
133		xp1st	$⊢ 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)})$
134		elmapfn	$⊢ 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
135	28 133 134	3syl	$⊢ φ \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
136	135	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
137		1ex	$⊢ 1 \in V$
138		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)]$
139	137 138	ax-mp	$⊢ (2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)]$
140		c0ex	$⊢ 0 \in V$
141		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
142	140 141	ax-mp	$⊢ (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
143	139 142	pm3.2i	$⊢ ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)] \land (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)])$
144		imain	$⊢ Fun {2^{nd} (1^{st} (U))}^{-1} \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
145	34 41 144	3syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
146	67	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (U)) [\emptyset]$
147		ima0	$⊢ 2^{nd} (1^{st} (U)) [\emptyset] = \emptyset$
148	146 147	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
149	145 148	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = \emptyset$
150		fnun	$⊢ (((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)] \land (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)])$
151	143 149 150	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)])$
152		imaundi	$⊢ 2^{nd} (1^{st} (U)) [(1 \dots M) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
153	58	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = 2^{nd} (1^{st} (U)) [(1 \dots M) \cup (M + 1 \dots N)]$
154	153 37	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cup (M + 1 \dots N)] = (1 \dots N)$
155	152 154	eqtr3id	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = (1 \dots N)$
156	155	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
157	151 156	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
158	157	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
159		ovexd	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to (1 \dots N) \in V$
160		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
161		eqidd	$⊢ ((φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) = 1^{st} (1^{st} (U)) (y)$
162		fvun2	$⊢ ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)] \land (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \land (2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = \emptyset \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)])) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) (y)$
163	139 142 162	mp3an12	$⊢ (2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = \emptyset \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) (y)$
164	149 163	sylan	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) (y)$
165	140	fvconst2	$⊢ y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \to (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) (y) = 0$
166	165	adantl	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) (y) = 0$
167	164 166	eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) (y) = 0$
168	167	adantr	$⊢ ((φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \land y \in (1 \dots N)) \to ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\})) (y) = 0$
169	136 158 159 159 160 161 168	ofval	$⊢ ((φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \land y \in (1 \dots N)) \to (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))) (y) = 1^{st} (1^{st} (U)) (y) + 0$
170	132 169	mpdan	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}))) (y) = 1^{st} (1^{st} (U)) (y) + 0$
171		elmapi	$⊢ 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
172	28 133 171	3syl	$⊢ φ \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
173	172	ffvelcdmda	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in (0 ..^K)$
174		elfzonn0	$⊢ 1^{st} (1^{st} (U)) (y) \in (0 ..^K) \to 1^{st} (1^{st} (U)) (y) \in ℕ_{0}$
175	173 174	syl	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in ℕ_{0}$
176	175	nn0cnd	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in ℂ$
177	176	addridd	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) + 0 = 1^{st} (1^{st} (U)) (y)$
178	132 177	syldan	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to 1^{st} (1^{st} (U)) (y) + 0 = 1^{st} (1^{st} (U)) (y)$
179	126 170 178	3eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to F (M) (y) = 1^{st} (1^{st} (U)) (y)$
180	76 179	syldan	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to F (M) (y) = 1^{st} (1^{st} (U)) (y)$
181		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
182	181	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
183	182	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
184	183	csbeq1d	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
185		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
186		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
187	186	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
188	187	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
189	186	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
190	189	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
191	188 190	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
192	185 191	oveq12d	$⊢ t = T \to 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\})) = 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\}))$
193	192	csbeq2dv	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
194	184 193	eqtrd	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
195	194	mpteq2dv	$⊢ t = T \to (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\})))) = (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\}))))$
196	195	eqeq2d	$⊢ t = T \to (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\})))) \leftrightarrow 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\})))))$
197	196 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land 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\})))))$
198	197	simprbi	$⊢ T \in S \to 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\}))))$
199	4 198	syl	$⊢ φ \to 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\}))))$
200		breq1	$⊢ y = M \to (y < 2^{nd} (T) \leftrightarrow M < 2^{nd} (T))$
201	200 97	ifbieq1d	$⊢ y = M \to if (y < 2^{nd} (T), y, y + 1) = if (M < 2^{nd} (T), M, y + 1)$
202	105 5	breqtrrd	$⊢ φ \to M < 2^{nd} (T)$
203	202	iftrued	$⊢ φ \to if (M < 2^{nd} (T), M, y + 1) = M$
204	201 203	sylan9eqr	$⊢ (φ \land y = M) \to if (y < 2^{nd} (T), y, y + 1) = M$
205	204	csbeq1d	$⊢ (φ \land y = M) \to ⦋ 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\}))) = ⦋ M / 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\})))$
206	110	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M)]$
207	206	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}$
208	114	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
209	208	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}$
210	207 209	uneq12d	$⊢ j = M \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
211	210	oveq2d	$⊢ j = M \to 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\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
212	211	adantl	$⊢ (φ \land j = M) \to 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\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
213	8 212	csbied	$⊢ φ \to ⦋ M / 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\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
214	213	adantr	$⊢ (φ \land y = M) \to ⦋ M / 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\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
215	205 214	eqtrd	$⊢ (φ \land y = M) \to ⦋ 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\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
216		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) \in V$
217	199 215 8 216	fvmptd	$⊢ φ \to F (M) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
218	217	fveq1d	$⊢ φ \to F (M) (y) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (y)$
219	218	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to F (M) (y) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (y)$
220	24	sselda	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to y \in (1 \dots N)$
221		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
222		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
223	14 221 222	3syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
224	223	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
225		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
226	137 225	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
227		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
228	140 227	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
229	226 228	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
230		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})$
231	230	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
232		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
233	20 231 232	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
234	67	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
235		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
236	234 235	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
237	233 236	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
238		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
239	229 237 238	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
240		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
241	58	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)]$
242		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)$
243		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)$
244	20 242 243	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
245	241 244	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)] = (1 \dots N)$
246	240 245	eqtr3id	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N)$
247	246	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
248	239 247	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
249	248	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
250		ovexd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to (1 \dots N) \in V$
251		eqidd	$⊢ ((φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) = 1^{st} (1^{st} (T)) (y)$
252		fvun1	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y)$
253	226 228 252	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y)$
254	237 253	sylan	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (y) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y)$
255	137	fvconst2	$⊢ y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y) = 1$
256	255	adantl	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y) = 1$
257	254 256	eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (y) = 1$
258	257	adantr	$⊢ ((φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \land y \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (y) = 1$
259	224 249 250 250 160 251 258	ofval	$⊢ ((φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \land y \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (y) = 1^{st} (1^{st} (T)) (y) + 1$
260	220 259	mpdan	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (y) = 1^{st} (1^{st} (T)) (y) + 1$
261	219 260	eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to F (M) (y) = 1^{st} (1^{st} (T)) (y) + 1$
262	261	adantrr	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to F (M) (y) = 1^{st} (1^{st} (T)) (y) + 1$
263	1	nngt0d	$⊢ φ \to 0 < N$
264	263 7	breqtrrd	$⊢ φ \to 0 < 2^{nd} (U)$
265	1 2 6 264	poimirlem5	$⊢ φ \to F (0) = 1^{st} (1^{st} (U))$
266	263 5	breqtrrd	$⊢ φ \to 0 < 2^{nd} (T)$
267	1 2 4 266	poimirlem5	$⊢ φ \to F (0) = 1^{st} (1^{st} (T))$
268	265 267	eqtr3d	$⊢ φ \to 1^{st} (1^{st} (U)) = 1^{st} (1^{st} (T))$
269	268	fveq1d	$⊢ φ \to 1^{st} (1^{st} (U)) (y) = 1^{st} (1^{st} (T)) (y)$
270	269	adantr	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to 1^{st} (1^{st} (U)) (y) = 1^{st} (1^{st} (T)) (y)$
271	180 262 270	3eqtr3d	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to 1^{st} (1^{st} (T)) (y) + 1 = 1^{st} (1^{st} (T)) (y)$
272		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
273	14 221 272	3syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
274	273	ffvelcdmda	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in (0 ..^K)$
275		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (y) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (y) \in ℕ_{0}$
276	274 275	syl	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in ℕ_{0}$
277	276	nn0red	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in ℝ$
278	277	ltp1d	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) < 1^{st} (1^{st} (T)) (y) + 1$
279	277 278	gtned	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) + 1 \neq 1^{st} (1^{st} (T)) (y)$
280	220 279	syldan	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to 1^{st} (1^{st} (T)) (y) + 1 \neq 1^{st} (1^{st} (T)) (y)$
281	280	neneqd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to \neg 1^{st} (1^{st} (T)) (y) + 1 = 1^{st} (1^{st} (T)) (y)$
282	281	adantrr	$⊢ (φ \land (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])) \to \neg 1^{st} (1^{st} (T)) (y) + 1 = 1^{st} (1^{st} (T)) (y)$
283	271 282	pm2.65da	$⊢ φ \to \neg (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])$
284		iman	$⊢ (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to y \in 2^{nd} (1^{st} (U)) [(1 \dots M)]) \leftrightarrow \neg (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \land \neg y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])$
285	283 284	sylibr	$⊢ φ \to (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])$
286	285	ssrdv	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots M)]$

Metamath Proof Explorer

Theorem poimirlem12

Proof