poimirlem11

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the first 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$
	poimirlem11.3	$⊢ φ \to 2^{nd} (T) = 0$
	poimirlem11.4	$⊢ φ \to U \in S$
	poimirlem11.5	$⊢ φ \to 2^{nd} (U) = 0$
	poimirlem11.6	$⊢ φ \to M \in (1 \dots N)$
Assertion	poimirlem11	$⊢ φ \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		poimirlem11.3	$⊢ φ \to 2^{nd} (T) = 0$
6		poimirlem11.4	$⊢ φ \to U \in S$
7		poimirlem11.5	$⊢ φ \to 2^{nd} (U) = 0$
8		poimirlem11.6	$⊢ φ \to M \in (1 \dots N)$
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	4 12	syl	$⊢ φ \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))$
14		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)\})$
15	13 14	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
16		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)\}$
17	15 16	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
18		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
19		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))$
20	18 19	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)$
21	17 20	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
22		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)$
23	21 22	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
24	23	frnd	$⊢ φ \to ran 2^{nd} (1^{st} (T)) \subseteq (1 \dots N)$
25	10 24	sstrid	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq (1 \dots N)$
26		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))$
27	26 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))$
28	6 27	syl	$⊢ φ \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		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)\})$
30	28 29	syl	$⊢ φ \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	30 31	syl	$⊢ φ \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		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)$
38	36 37	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
39		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)$
40	38 39	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = (1 \dots N)$
41	25 40	sseqtrrd	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots N)]$
42	41	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)]$
43		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})$
44	43	simprbi	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (U))}^{-1}$
45	36 44	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (U))}^{-1}$
46		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)]$
47	45 46	syl	$⊢ φ \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)]$
48		difun2	$⊢ ((M + 1 \dots N) \cup (1 \dots M)) ∖ (1 \dots M) = (M + 1 \dots N) ∖ (1 \dots M)$
49		fzsplit	$⊢ M \in (1 \dots N) \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
50	8 49	syl	$⊢ φ \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
51		uncom	$⊢ (1 \dots M) \cup (M + 1 \dots N) = (M + 1 \dots N) \cup (1 \dots M)$
52	50 51	eqtrdi	$⊢ φ \to (1 \dots N) = (M + 1 \dots N) \cup (1 \dots M)$
53	52	difeq1d	$⊢ φ \to (1 \dots N) ∖ (1 \dots M) = ((M + 1 \dots N) \cup (1 \dots M)) ∖ (1 \dots M)$
54		incom	$⊢ (M + 1 \dots N) \cap (1 \dots M) = (1 \dots M) \cap (M + 1 \dots N)$
55		elfznn	$⊢ M \in (1 \dots N) \to M \in ℕ$
56	8 55	syl	$⊢ φ \to M \in ℕ$
57	56	nnred	$⊢ φ \to M \in ℝ$
58	57	ltp1d	$⊢ φ \to M < M + 1$
59		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
60	58 59	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
61	54 60	eqtrid	$⊢ φ \to (M + 1 \dots N) \cap (1 \dots M) = \emptyset$
62		disj3	$⊢ (M + 1 \dots N) \cap (1 \dots M) = \emptyset \leftrightarrow (M + 1 \dots N) = (M + 1 \dots N) ∖ (1 \dots M)$
63	61 62	sylib	$⊢ φ \to (M + 1 \dots N) = (M + 1 \dots N) ∖ (1 \dots M)$
64	48 53 63	3eqtr4a	$⊢ φ \to (1 \dots N) ∖ (1 \dots M) = (M + 1 \dots N)$
65	64	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N) ∖ (1 \dots M)] = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
66	47 65	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)]$
67	42 66	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)]$
68	67	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)]$
69	9 68	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)]$
70		fveq2	$⊢ t = U \to 2^{nd} (t) = 2^{nd} (U)$
71	70	breq2d	$⊢ t = U \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (U))$
72	71	ifbid	$⊢ t = U \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (U), y, y + 1)$
73	72	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\})))$
74		2fveq3	$⊢ t = U \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (U))$
75		2fveq3	$⊢ t = U \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (U))$
76	75	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (U)) [(1 \dots j)]$
77	76	xpeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}$
78	75	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(j + 1 \dots N)]$
79	78	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\}$
80	77 79	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\})$
81	74 80	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\}))$
82	81	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\})))$
83	73 82	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\})))$
84	83	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\}))))$
85	84	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\})))))$
86	85 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\})))))$
87	86	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\}))))$
88	6 87	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\}))))$
89		breq12	$⊢ (y = M - 1 \land 2^{nd} (U) = 0) \to (y < 2^{nd} (U) \leftrightarrow M - 1 < 0)$
90	7 89	sylan2	$⊢ (y = M - 1 \land φ) \to (y < 2^{nd} (U) \leftrightarrow M - 1 < 0)$
91	90	ancoms	$⊢ (φ \land y = M - 1) \to (y < 2^{nd} (U) \leftrightarrow M - 1 < 0)$
92		oveq1	$⊢ y = M - 1 \to y + 1 = M - 1 + 1$
93	56	nncnd	$⊢ φ \to M \in ℂ$
94		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
95	93 94	syl	$⊢ φ \to M - 1 + 1 = M$
96	92 95	sylan9eqr	$⊢ (φ \land y = M - 1) \to y + 1 = M$
97	91 96	ifbieq2d	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (U), y, y + 1) = if (M - 1 < 0, y, M)$
98	56	nnzd	$⊢ φ \to M \in ℤ$
99	1	nnzd	$⊢ φ \to N \in ℤ$
100		elfzm1b	$⊢ (M \in ℤ \land N \in ℤ) \to (M \in (1 \dots N) \leftrightarrow M - 1 \in (0 \dots N - 1))$
101	98 99 100	syl2anc	$⊢ φ \to (M \in (1 \dots N) \leftrightarrow M - 1 \in (0 \dots N - 1))$
102	8 101	mpbid	$⊢ φ \to M - 1 \in (0 \dots N - 1)$
103		elfzle1	$⊢ M - 1 \in (0 \dots N - 1) \to 0 \leq M - 1$
104	102 103	syl	$⊢ φ \to 0 \leq M - 1$
105		0red	$⊢ φ \to 0 \in ℝ$
106		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
107	56 106	syl	$⊢ φ \to M - 1 \in ℕ_{0}$
108	107	nn0red	$⊢ φ \to M - 1 \in ℝ$
109	105 108	lenltd	$⊢ φ \to (0 \leq M - 1 \leftrightarrow \neg M - 1 < 0)$
110	104 109	mpbid	$⊢ φ \to \neg M - 1 < 0$
111	110	iffalsed	$⊢ φ \to if (M - 1 < 0, y, M) = M$
112	111	adantr	$⊢ (φ \land y = M - 1) \to if (M - 1 < 0, y, M) = M$
113	97 112	eqtrd	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (U), y, y + 1) = M$
114	113	csbeq1d	$⊢ (φ \land y = M - 1) \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\})))$
115		oveq2	$⊢ j = M \to (1 \dots j) = (1 \dots M)$
116	115	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(1 \dots j)] = 2^{nd} (1^{st} (U)) [(1 \dots M)]$
117	116	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}$
118		oveq1	$⊢ j = M \to j + 1 = M + 1$
119	118	oveq1d	$⊢ j = M \to (j + 1 \dots N) = (M + 1 \dots N)$
120	119	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (U)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
121	120	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\}$
122	117 121	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\})$
123	122	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\}))$
124	123	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\}))$
125	8 124	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\}))$
126	125	adantr	$⊢ (φ \land y = M - 1) \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\}))$
127	114 126	eqtrd	$⊢ (φ \land y = M - 1) \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\}))$
128		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$
129	88 127 102 128	fvmptd	$⊢ φ \to F (M - 1) = 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\}))$
130	129	fveq1d	$⊢ φ \to F (M - 1) (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)$
131	130	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to F (M - 1) (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)$
132		imassrn	$⊢ 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \subseteq ran 2^{nd} (1^{st} (U))$
133		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)$
134	36 133	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) ⟶ (1 \dots N)$
135	134	frnd	$⊢ φ \to ran 2^{nd} (1^{st} (U)) \subseteq (1 \dots N)$
136	132 135	sstrid	$⊢ φ \to 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \subseteq (1 \dots N)$
137	136	sselda	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to y \in (1 \dots N)$
138		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)})$
139	30 138	syl	$⊢ φ \to 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)})$
140		elmapfn	$⊢ 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
141	139 140	syl	$⊢ φ \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
142	141	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to 1^{st} (1^{st} (U)) Fn (1 \dots N)$
143		1ex	$⊢ 1 \in V$
144		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)]$
145	143 144	ax-mp	$⊢ (2^{nd} (1^{st} (U)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (U)) [(1 \dots M)]$
146		c0ex	$⊢ 0 \in V$
147		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)]$
148	146 147	ax-mp	$⊢ (2^{nd} (1^{st} (U)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]$
149	145 148	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)])$
150		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)]$
151	45 150	syl	$⊢ φ \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)]$
152	60	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (U)) [\emptyset]$
153		ima0	$⊢ 2^{nd} (1^{st} (U)) [\emptyset] = \emptyset$
154	152 153	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
155	151 154	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M)] \cap 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = \emptyset$
156		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)])$
157	149 155 156	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)])$
158		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)]$
159	50	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots N)] = 2^{nd} (1^{st} (U)) [(1 \dots M) \cup (M + 1 \dots N)]$
160	159 40	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M) \cup (M + 1 \dots N)] = (1 \dots N)$
161	158 160	eqtr3id	$⊢ φ \to 2^{nd} (1^{st} (U)) [(1 \dots M)] \cup 2^{nd} (1^{st} (U)) [(M + 1 \dots N)] = (1 \dots N)$
162	161	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))$
163	157 162	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)$
164	163	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)$
165		ovexd	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to (1 \dots N) \in V$
166		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
167		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)$
168		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)$
169	145 148 168	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)$
170	155 169	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)$
171	146	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$
172	171	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$
173	170 172	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$
174	173	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$
175	142 164 165 165 166 167 174	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$
176	137 175	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$
177		elmapi	$⊢ 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
178	139 177	syl	$⊢ φ \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
179	178	ffvelcdmda	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in (0 ..^K)$
180		elfzonn0	$⊢ 1^{st} (1^{st} (U)) (y) \in (0 ..^K) \to 1^{st} (1^{st} (U)) (y) \in ℕ_{0}$
181	179 180	syl	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in ℕ_{0}$
182	181	nn0cnd	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (U)) (y) \in ℂ$
183	137 182	syldan	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to 1^{st} (1^{st} (U)) (y) \in ℂ$
184	183	addridd	$⊢ (φ \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)$
185	131 176 184	3eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (U)) [(M + 1 \dots N)]) \to F (M - 1) (y) = 1^{st} (1^{st} (U)) (y)$
186	69 185	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 - 1) (y) = 1^{st} (1^{st} (U)) (y)$
187		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
188	187	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
189	188	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
190	189	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\})))$
191		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
192		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
193	192	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
194	193	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
195	192	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
196	195	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\}$
197	194 196	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\})$
198	191 197	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\}))$
199	198	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\})))$
200	190 199	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\})))$
201	200	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\}))))$
202	201	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\})))))$
203	202 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\})))))$
204	203	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\}))))$
205	4 204	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\}))))$
206		breq12	$⊢ (y = M - 1 \land 2^{nd} (T) = 0) \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 0)$
207	5 206	sylan2	$⊢ (y = M - 1 \land φ) \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 0)$
208	207	ancoms	$⊢ (φ \land y = M - 1) \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 0)$
209	208 96	ifbieq2d	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (T), y, y + 1) = if (M - 1 < 0, y, M)$
210	209 112	eqtrd	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (T), y, y + 1) = M$
211	210	csbeq1d	$⊢ (φ \land y = M - 1) \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\})))$
212	115	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M)]$
213	212	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}$
214	119	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
215	214	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\}$
216	213 215	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\})$
217	216	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\}))$
218	217	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\}))$
219	8 218	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\}))$
220	219	adantr	$⊢ (φ \land y = M - 1) \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\}))$
221	211 220	eqtrd	$⊢ (φ \land y = M - 1) \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\}))$
222		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$
223	205 221 102 222	fvmptd	$⊢ φ \to F (M - 1) = 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\}))$
224	223	fveq1d	$⊢ φ \to F (M - 1) (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)$
225	224	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to F (M - 1) (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)$
226	25	sselda	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to y \in (1 \dots N)$
227		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)})$
228	15 227	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
229		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
230	228 229	syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
231	230	adantr	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
232		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
233	143 232	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
234		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)]$
235	146 234	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
236	233 235	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)])$
237		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})$
238	237	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
239	21 238	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (T))}^{-1}$
240		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)]$
241	239 240	syl	$⊢ φ \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)]$
242	60	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
243		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
244	242 243	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
245	241 244	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
246		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)])$
247	236 245 246	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)])$
248		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)]$
249	50	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)]$
250		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)$
251	21 250	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
252		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)$
253	251 252	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
254	249 253	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)] = (1 \dots N)$
255	248 254	eqtr3id	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N)$
256	255	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))$
257	247 256	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)$
258	257	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)$
259		ovexd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to (1 \dots N) \in V$
260		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)$
261		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)$
262	233 235 261	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)$
263	245 262	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)$
264	143	fvconst2	$⊢ y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (y) = 1$
265	264	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$
266	263 265	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$
267	266	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$
268	231 258 259 259 166 260 267	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$
269	226 268	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$
270	225 269	eqtrd	$⊢ (φ \land y \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to F (M - 1) (y) = 1^{st} (1^{st} (T)) (y) + 1$
271	270	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 - 1) (y) = 1^{st} (1^{st} (T)) (y) + 1$
272	1 2 3 6 7	poimirlem10	$⊢ φ \to F (N - 1) -_{f} ((1 \dots N) \times \{1\}) = 1^{st} (1^{st} (U))$
273	1 2 3 4 5	poimirlem10	$⊢ φ \to F (N - 1) -_{f} ((1 \dots N) \times \{1\}) = 1^{st} (1^{st} (T))$
274	272 273	eqtr3d	$⊢ φ \to 1^{st} (1^{st} (U)) = 1^{st} (1^{st} (T))$
275	274	fveq1d	$⊢ φ \to 1^{st} (1^{st} (U)) (y) = 1^{st} (1^{st} (T)) (y)$
276	275	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)$
277	186 271 276	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)$
278		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
279	228 278	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
280	279	ffvelcdmda	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in (0 ..^K)$
281		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (y) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (y) \in ℕ_{0}$
282	280 281	syl	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in ℕ_{0}$
283	282	nn0red	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) \in ℝ$
284	283	ltp1d	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) < 1^{st} (1^{st} (T)) (y) + 1$
285	283 284	gtned	$⊢ (φ \land y \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (y) + 1 \neq 1^{st} (1^{st} (T)) (y)$
286	226 285	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)$
287	286	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)$
288	287	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)$
289	277 288	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)])$
290		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)])$
291	289 290	sylibr	$⊢ φ \to (y \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to y \in 2^{nd} (1^{st} (U)) [(1 \dots M)])$
292	291	ssrdv	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \subseteq 2^{nd} (1^{st} (U)) [(1 \dots M)]$

Metamath Proof Explorer

Theorem poimirlem11

Proof