smatrcl

Description: Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

	Ref	Expression
Hypotheses	smat.s	$⊢ S = K {subMat}_{1} (A) L$
	smat.m	$⊢ φ \to M \in ℕ$
	smat.n	$⊢ φ \to N \in ℕ$
	smat.k	$⊢ φ \to K \in (1 \dots M)$
	smat.l	$⊢ φ \to L \in (1 \dots N)$
	smat.a	$⊢ φ \to A \in (B^{((1 \dots M) \times (1 \dots N))})$
Assertion	smatrcl	$⊢ φ \to S \in (B^{((1 \dots M - 1) \times (1 \dots N - 1))})$

Proof

Step	Hyp	Ref	Expression
1		smat.s	$⊢ S = K {subMat}_{1} (A) L$
2		smat.m	$⊢ φ \to M \in ℕ$
3		smat.n	$⊢ φ \to N \in ℕ$
4		smat.k	$⊢ φ \to K \in (1 \dots M)$
5		smat.l	$⊢ φ \to L \in (1 \dots N)$
6		smat.a	$⊢ φ \to A \in (B^{((1 \dots M) \times (1 \dots N))})$
7		elmapi	$⊢ A \in (B^{((1 \dots M) \times (1 \dots N))}) \to A : (1 \dots M) \times (1 \dots N) ⟶ B$
8		ffun	$⊢ A : (1 \dots M) \times (1 \dots N) ⟶ B \to Fun A$
9	6 7 8	3syl	$⊢ φ \to Fun A$
10		eqid	$⊢ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) = (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
11	10	mpofun	$⊢ Fun (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
12	11	a1i	$⊢ φ \to Fun (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
13		funco	$⊢ (Fun A \land Fun (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) \to Fun (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩))$
14	9 12 13	syl2anc	$⊢ φ \to Fun (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩))$
15		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
16	15 4	sselid	$⊢ φ \to K \in ℕ$
17		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
18	17 5	sselid	$⊢ φ \to L \in ℕ$
19		smatfval	$⊢ (K \in ℕ \land L \in ℕ \land A \in (B^{((1 \dots M) \times (1 \dots N))})) \to K {subMat}_{1} (A) L = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
20	16 18 6 19	syl3anc	$⊢ φ \to K {subMat}_{1} (A) L = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
21	1 20	syl5eq	$⊢ φ \to S = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
22	21	funeqd	$⊢ φ \to (Fun S \leftrightarrow Fun (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)))$
23	14 22	mpbird	$⊢ φ \to Fun S$
24		fdmrn	$⊢ Fun S \leftrightarrow S : dom S ⟶ ran S$
25	23 24	sylib	$⊢ φ \to S : dom S ⟶ ran S$
26	21	dmeqd	$⊢ φ \to dom S = dom (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩))$
27		dmco	$⊢ dom (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) = {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [dom A]$
28		fdm	$⊢ A : (1 \dots M) \times (1 \dots N) ⟶ B \to dom A = (1 \dots M) \times (1 \dots N)$
29	6 7 28	3syl	$⊢ φ \to dom A = (1 \dots M) \times (1 \dots N)$
30	29	imaeq2d	$⊢ φ \to {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [dom A] = {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [(1 \dots M) \times (1 \dots N)]$
31	30	eleq2d	$⊢ φ \to (x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [dom A] \leftrightarrow x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [(1 \dots M) \times (1 \dots N)])$
32		opex	$⊢ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩ \in V$
33	10 32	fnmpoi	$⊢ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) Fn (ℕ \times ℕ)$
34		elpreima	$⊢ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) Fn (ℕ \times ℕ) \to (x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [(1 \dots M) \times (1 \dots N)] \leftrightarrow (x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))))$
35	33 34	ax-mp	$⊢ x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [(1 \dots M) \times (1 \dots N)] \leftrightarrow (x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)))$
36	35	a1i	$⊢ φ \to (x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [(1 \dots M) \times (1 \dots N)] \leftrightarrow (x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))))$
37		simplr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
38	37	fveq2d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) = (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨1^{st} (x), 2^{nd} (x)⟩)$
39		df-ov	$⊢ 1^{st} (x) (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) 2^{nd} (x) = (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨1^{st} (x), 2^{nd} (x)⟩)$
40	38 39	eqtr4di	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) = 1^{st} (x) (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) 2^{nd} (x)$
41		breq1	$⊢ i = 1^{st} (x) \to (i < K \leftrightarrow 1^{st} (x) < K)$
42		id	$⊢ i = 1^{st} (x) \to i = 1^{st} (x)$
43		oveq1	$⊢ i = 1^{st} (x) \to i + 1 = 1^{st} (x) + 1$
44	41 42 43	ifbieq12d	$⊢ i = 1^{st} (x) \to if (i < K, i, i + 1) = if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1)$
45	44	opeq1d	$⊢ i = 1^{st} (x) \to ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩ = ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (j < L, j, j + 1)⟩$
46		breq1	$⊢ j = 2^{nd} (x) \to (j < L \leftrightarrow 2^{nd} (x) < L)$
47		id	$⊢ j = 2^{nd} (x) \to j = 2^{nd} (x)$
48		oveq1	$⊢ j = 2^{nd} (x) \to j + 1 = 2^{nd} (x) + 1$
49	46 47 48	ifbieq12d	$⊢ j = 2^{nd} (x) \to if (j < L, j, j + 1) = if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)$
50	49	opeq2d	$⊢ j = 2^{nd} (x) \to ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (j < L, j, j + 1)⟩ = ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩$
51		opex	$⊢ ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩ \in V$
52	45 50 10 51	ovmpo	$⊢ (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \to 1^{st} (x) (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) 2^{nd} (x) = ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩$
53	52	adantl	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 1^{st} (x) (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) 2^{nd} (x) = ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩$
54	40 53	eqtrd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) = ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩$
55	54	eleq1d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)) \leftrightarrow ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩ \in ((1 \dots M) \times (1 \dots N)))$
56		opelxp	$⊢ ⟨if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1), if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1)⟩ \in ((1 \dots M) \times (1 \dots N)) \leftrightarrow (if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1) \in (1 \dots M) \land if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1) \in (1 \dots N))$
57	55 56	bitrdi	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)) \leftrightarrow (if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1) \in (1 \dots M) \land if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1) \in (1 \dots N)))$
58		ifel	$⊢ if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1) \in (1 \dots M) \leftrightarrow ((1^{st} (x) < K \land 1^{st} (x) \in (1 \dots M)) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) + 1 \in (1 \dots M)))$
59		simplrl	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \in ℕ$
60	59	nnred	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \in ℝ$
61	16	nnred	$⊢ φ \to K \in ℝ$
62	61	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to K \in ℝ$
63	2	nnred	$⊢ φ \to M \in ℝ$
64	63	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to M \in ℝ$
65		simpr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) < K$
66	60 62 65	ltled	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \leq K$
67		elfzle2	$⊢ K \in (1 \dots M) \to K \leq M$
68	4 67	syl	$⊢ φ \to K \leq M$
69	68	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to K \leq M$
70	60 62 64 66 69	letrd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \leq M$
71	59 70	jca	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M)$
72	2	nnzd	$⊢ φ \to M \in ℤ$
73		fznn	$⊢ M \in ℤ \to (1^{st} (x) \in (1 \dots M) \leftrightarrow (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M))$
74	72 73	syl	$⊢ φ \to (1^{st} (x) \in (1 \dots M) \leftrightarrow (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M))$
75	74	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to (1^{st} (x) \in (1 \dots M) \leftrightarrow (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M))$
76	71 75	mpbird	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \in (1 \dots M)$
77	60 62 64 65 69	ltletrd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) < M$
78	2	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to M \in ℕ$
79		nnltlem1	$⊢ (1^{st} (x) \in ℕ \land M \in ℕ) \to (1^{st} (x) < M \leftrightarrow 1^{st} (x) \leq M - 1)$
80	59 78 79	syl2anc	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to (1^{st} (x) < M \leftrightarrow 1^{st} (x) \leq M - 1)$
81	77 80	mpbid	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to 1^{st} (x) \leq M - 1$
82	76 81	2thd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 1^{st} (x) < K) \to (1^{st} (x) \in (1 \dots M) \leftrightarrow 1^{st} (x) \leq M - 1)$
83	82	pm5.32da	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((1^{st} (x) < K \land 1^{st} (x) \in (1 \dots M)) \leftrightarrow (1^{st} (x) < K \land 1^{st} (x) \leq M - 1))$
84		fznn	$⊢ M \in ℤ \to (1^{st} (x) + 1 \in (1 \dots M) \leftrightarrow (1^{st} (x) + 1 \in ℕ \land 1^{st} (x) + 1 \leq M))$
85	72 84	syl	$⊢ φ \to (1^{st} (x) + 1 \in (1 \dots M) \leftrightarrow (1^{st} (x) + 1 \in ℕ \land 1^{st} (x) + 1 \leq M))$
86	85	ad2antrr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (1^{st} (x) + 1 \in (1 \dots M) \leftrightarrow (1^{st} (x) + 1 \in ℕ \land 1^{st} (x) + 1 \leq M))$
87		simprl	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 1^{st} (x) \in ℕ$
88	87	peano2nnd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 1^{st} (x) + 1 \in ℕ$
89	88	biantrurd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (1^{st} (x) + 1 \leq M \leftrightarrow (1^{st} (x) + 1 \in ℕ \land 1^{st} (x) + 1 \leq M))$
90	87	nnzd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 1^{st} (x) \in ℤ$
91	72	ad2antrr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to M \in ℤ$
92		zltp1le	$⊢ (1^{st} (x) \in ℤ \land M \in ℤ) \to (1^{st} (x) < M \leftrightarrow 1^{st} (x) + 1 \leq M)$
93		zltlem1	$⊢ (1^{st} (x) \in ℤ \land M \in ℤ) \to (1^{st} (x) < M \leftrightarrow 1^{st} (x) \leq M - 1)$
94	92 93	bitr3d	$⊢ (1^{st} (x) \in ℤ \land M \in ℤ) \to (1^{st} (x) + 1 \leq M \leftrightarrow 1^{st} (x) \leq M - 1)$
95	90 91 94	syl2anc	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (1^{st} (x) + 1 \leq M \leftrightarrow 1^{st} (x) \leq M - 1)$
96	86 89 95	3bitr2d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (1^{st} (x) + 1 \in (1 \dots M) \leftrightarrow 1^{st} (x) \leq M - 1)$
97	96	anbi2d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((\neg 1^{st} (x) < K \land 1^{st} (x) + 1 \in (1 \dots M)) \leftrightarrow (\neg 1^{st} (x) < K \land 1^{st} (x) \leq M - 1))$
98	83 97	orbi12d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (((1^{st} (x) < K \land 1^{st} (x) \in (1 \dots M)) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) + 1 \in (1 \dots M))) \leftrightarrow ((1^{st} (x) < K \land 1^{st} (x) \leq M - 1) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) \leq M - 1)))$
99		pm4.42	$⊢ 1^{st} (x) \leq M - 1 \leftrightarrow ((1^{st} (x) \leq M - 1 \land 1^{st} (x) < K) \lor (1^{st} (x) \leq M - 1 \land \neg 1^{st} (x) < K))$
100		ancom	$⊢ (1^{st} (x) \leq M - 1 \land 1^{st} (x) < K) \leftrightarrow (1^{st} (x) < K \land 1^{st} (x) \leq M - 1)$
101		ancom	$⊢ (1^{st} (x) \leq M - 1 \land \neg 1^{st} (x) < K) \leftrightarrow (\neg 1^{st} (x) < K \land 1^{st} (x) \leq M - 1)$
102	100 101	orbi12i	$⊢ ((1^{st} (x) \leq M - 1 \land 1^{st} (x) < K) \lor (1^{st} (x) \leq M - 1 \land \neg 1^{st} (x) < K)) \leftrightarrow ((1^{st} (x) < K \land 1^{st} (x) \leq M - 1) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) \leq M - 1))$
103	99 102	bitri	$⊢ 1^{st} (x) \leq M - 1 \leftrightarrow ((1^{st} (x) < K \land 1^{st} (x) \leq M - 1) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) \leq M - 1))$
104	98 103	bitr4di	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (((1^{st} (x) < K \land 1^{st} (x) \in (1 \dots M)) \lor (\neg 1^{st} (x) < K \land 1^{st} (x) + 1 \in (1 \dots M))) \leftrightarrow 1^{st} (x) \leq M - 1)$
105	58 104	syl5bb	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1) \in (1 \dots M) \leftrightarrow 1^{st} (x) \leq M - 1)$
106		ifel	$⊢ if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1) \in (1 \dots N) \leftrightarrow ((2^{nd} (x) < L \land 2^{nd} (x) \in (1 \dots N)) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) + 1 \in (1 \dots N)))$
107		simplrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \in ℕ$
108	107	nnred	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \in ℝ$
109	18	nnred	$⊢ φ \to L \in ℝ$
110	109	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to L \in ℝ$
111	3	nnred	$⊢ φ \to N \in ℝ$
112	111	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to N \in ℝ$
113		simpr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) < L$
114	108 110 113	ltled	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \leq L$
115		elfzle2	$⊢ L \in (1 \dots N) \to L \leq N$
116	5 115	syl	$⊢ φ \to L \leq N$
117	116	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to L \leq N$
118	108 110 112 114 117	letrd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \leq N$
119	107 118	jca	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N)$
120	3	nnzd	$⊢ φ \to N \in ℤ$
121		fznn	$⊢ N \in ℤ \to (2^{nd} (x) \in (1 \dots N) \leftrightarrow (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N))$
122	120 121	syl	$⊢ φ \to (2^{nd} (x) \in (1 \dots N) \leftrightarrow (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N))$
123	122	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to (2^{nd} (x) \in (1 \dots N) \leftrightarrow (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N))$
124	119 123	mpbird	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \in (1 \dots N)$
125	108 110 112 113 117	ltletrd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) < N$
126	3	ad3antrrr	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to N \in ℕ$
127		nnltlem1	$⊢ (2^{nd} (x) \in ℕ \land N \in ℕ) \to (2^{nd} (x) < N \leftrightarrow 2^{nd} (x) \leq N - 1)$
128	107 126 127	syl2anc	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to (2^{nd} (x) < N \leftrightarrow 2^{nd} (x) \leq N - 1)$
129	125 128	mpbid	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to 2^{nd} (x) \leq N - 1$
130	124 129	2thd	$⊢ (((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land 2^{nd} (x) < L) \to (2^{nd} (x) \in (1 \dots N) \leftrightarrow 2^{nd} (x) \leq N - 1)$
131	130	pm5.32da	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((2^{nd} (x) < L \land 2^{nd} (x) \in (1 \dots N)) \leftrightarrow (2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1))$
132		fznn	$⊢ N \in ℤ \to (2^{nd} (x) + 1 \in (1 \dots N) \leftrightarrow (2^{nd} (x) + 1 \in ℕ \land 2^{nd} (x) + 1 \leq N))$
133	120 132	syl	$⊢ φ \to (2^{nd} (x) + 1 \in (1 \dots N) \leftrightarrow (2^{nd} (x) + 1 \in ℕ \land 2^{nd} (x) + 1 \leq N))$
134	133	ad2antrr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (2^{nd} (x) + 1 \in (1 \dots N) \leftrightarrow (2^{nd} (x) + 1 \in ℕ \land 2^{nd} (x) + 1 \leq N))$
135		simprr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 2^{nd} (x) \in ℕ$
136	135	peano2nnd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 2^{nd} (x) + 1 \in ℕ$
137	136	biantrurd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (2^{nd} (x) + 1 \leq N \leftrightarrow (2^{nd} (x) + 1 \in ℕ \land 2^{nd} (x) + 1 \leq N))$
138	135	nnzd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to 2^{nd} (x) \in ℤ$
139	120	ad2antrr	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to N \in ℤ$
140		zltp1le	$⊢ (2^{nd} (x) \in ℤ \land N \in ℤ) \to (2^{nd} (x) < N \leftrightarrow 2^{nd} (x) + 1 \leq N)$
141		zltlem1	$⊢ (2^{nd} (x) \in ℤ \land N \in ℤ) \to (2^{nd} (x) < N \leftrightarrow 2^{nd} (x) \leq N - 1)$
142	140 141	bitr3d	$⊢ (2^{nd} (x) \in ℤ \land N \in ℤ) \to (2^{nd} (x) + 1 \leq N \leftrightarrow 2^{nd} (x) \leq N - 1)$
143	138 139 142	syl2anc	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (2^{nd} (x) + 1 \leq N \leftrightarrow 2^{nd} (x) \leq N - 1)$
144	134 137 143	3bitr2d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (2^{nd} (x) + 1 \in (1 \dots N) \leftrightarrow 2^{nd} (x) \leq N - 1)$
145	144	anbi2d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((\neg 2^{nd} (x) < L \land 2^{nd} (x) + 1 \in (1 \dots N)) \leftrightarrow (\neg 2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1))$
146	131 145	orbi12d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (((2^{nd} (x) < L \land 2^{nd} (x) \in (1 \dots N)) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) + 1 \in (1 \dots N))) \leftrightarrow ((2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1)))$
147		pm4.42	$⊢ 2^{nd} (x) \leq N - 1 \leftrightarrow ((2^{nd} (x) \leq N - 1 \land 2^{nd} (x) < L) \lor (2^{nd} (x) \leq N - 1 \land \neg 2^{nd} (x) < L))$
148		ancom	$⊢ (2^{nd} (x) \leq N - 1 \land 2^{nd} (x) < L) \leftrightarrow (2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1)$
149		ancom	$⊢ (2^{nd} (x) \leq N - 1 \land \neg 2^{nd} (x) < L) \leftrightarrow (\neg 2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1)$
150	148 149	orbi12i	$⊢ ((2^{nd} (x) \leq N - 1 \land 2^{nd} (x) < L) \lor (2^{nd} (x) \leq N - 1 \land \neg 2^{nd} (x) < L)) \leftrightarrow ((2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1))$
151	147 150	bitri	$⊢ 2^{nd} (x) \leq N - 1 \leftrightarrow ((2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) \leq N - 1))$
152	146 151	bitr4di	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (((2^{nd} (x) < L \land 2^{nd} (x) \in (1 \dots N)) \lor (\neg 2^{nd} (x) < L \land 2^{nd} (x) + 1 \in (1 \dots N))) \leftrightarrow 2^{nd} (x) \leq N - 1)$
153	106 152	syl5bb	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to (if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1) \in (1 \dots N) \leftrightarrow 2^{nd} (x) \leq N - 1)$
154	105 153	anbi12d	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((if (1^{st} (x) < K, 1^{st} (x), 1^{st} (x) + 1) \in (1 \dots M) \land if (2^{nd} (x) < L, 2^{nd} (x), 2^{nd} (x) + 1) \in (1 \dots N)) \leftrightarrow (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1))$
155	57 154	bitrd	$⊢ ((φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \to ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)) \leftrightarrow (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1))$
156	155	pm5.32da	$⊢ (φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \to (((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1)))$
157		1zzd	$⊢ φ \to 1 \in ℤ$
158	72 157	zsubcld	$⊢ φ \to M - 1 \in ℤ$
159		fznn	$⊢ M - 1 \in ℤ \to (1^{st} (x) \in (1 \dots M - 1) \leftrightarrow (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M - 1))$
160	158 159	syl	$⊢ φ \to (1^{st} (x) \in (1 \dots M - 1) \leftrightarrow (1^{st} (x) \in ℕ \land 1^{st} (x) \leq M - 1))$
161	120 157	zsubcld	$⊢ φ \to N - 1 \in ℤ$
162		fznn	$⊢ N - 1 \in ℤ \to (2^{nd} (x) \in (1 \dots N - 1) \leftrightarrow (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N - 1))$
163	161 162	syl	$⊢ φ \to (2^{nd} (x) \in (1 \dots N - 1) \leftrightarrow (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N - 1))$
164	160 163	anbi12d	$⊢ φ \to ((1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1)) \leftrightarrow ((1^{st} (x) \in ℕ \land 1^{st} (x) \leq M - 1) \land (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N - 1)))$
165		an4	$⊢ ((1^{st} (x) \in ℕ \land 1^{st} (x) \leq M - 1) \land (2^{nd} (x) \in ℕ \land 2^{nd} (x) \leq N - 1)) \leftrightarrow ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1))$
166	164 165	bitrdi	$⊢ φ \to ((1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1)) \leftrightarrow ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1)))$
167	166	adantr	$⊢ (φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \to ((1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1)) \leftrightarrow ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (1^{st} (x) \leq M - 1 \land 2^{nd} (x) \leq N - 1)))$
168	156 167	bitr4d	$⊢ (φ \land x = ⟨1^{st} (x), 2^{nd} (x)⟩) \to (((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow (1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1)))$
169	168	pm5.32da	$⊢ φ \to ((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)))) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1))))$
170		elxp6	$⊢ x \in (ℕ \times ℕ) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ))$
171	170	anbi1i	$⊢ (x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow ((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N)))$
172		anass	$⊢ ((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ)) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))))$
173	171 172	bitri	$⊢ (x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land ((1^{st} (x) \in ℕ \land 2^{nd} (x) \in ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))))$
174		elxp6	$⊢ x \in ((1 \dots M - 1) \times (1 \dots N - 1)) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in (1 \dots M - 1) \land 2^{nd} (x) \in (1 \dots N - 1)))$
175	169 173 174	3bitr4g	$⊢ φ \to ((x \in (ℕ \times ℕ) \land (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (x) \in ((1 \dots M) \times (1 \dots N))) \leftrightarrow x \in ((1 \dots M - 1) \times (1 \dots N - 1)))$
176	31 36 175	3bitrd	$⊢ φ \to (x \in {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [dom A] \leftrightarrow x \in ((1 \dots M - 1) \times (1 \dots N - 1)))$
177	176	eqrdv	$⊢ φ \to {(i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)}^{-1} [dom A] = (1 \dots M - 1) \times (1 \dots N - 1)$
178	27 177	syl5eq	$⊢ φ \to dom (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) = (1 \dots M - 1) \times (1 \dots N - 1)$
179	26 178	eqtrd	$⊢ φ \to dom S = (1 \dots M - 1) \times (1 \dots N - 1)$
180	179	feq2d	$⊢ φ \to (S : dom S ⟶ ran S \leftrightarrow S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ ran S)$
181	25 180	mpbid	$⊢ φ \to S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ ran S$
182	21	rneqd	$⊢ φ \to ran S = ran (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩))$
183		rncoss	$⊢ ran (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) \subseteq ran A$
184	182 183	eqsstrdi	$⊢ φ \to ran S \subseteq ran A$
185		frn	$⊢ A : (1 \dots M) \times (1 \dots N) ⟶ B \to ran A \subseteq B$
186	6 7 185	3syl	$⊢ φ \to ran A \subseteq B$
187	184 186	sstrd	$⊢ φ \to ran S \subseteq B$
188		fss	$⊢ (S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ ran S \land ran S \subseteq B) \to S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ B$
189	181 187 188	syl2anc	$⊢ φ \to S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ B$
190		reldmmap	$⊢ Rel dom ↑_{𝑚}$
191	190	ovrcl	$⊢ A \in (B^{((1 \dots M) \times (1 \dots N))}) \to (B \in V \land (1 \dots M) \times (1 \dots N) \in V)$
192	6 191	syl	$⊢ φ \to (B \in V \land (1 \dots M) \times (1 \dots N) \in V)$
193	192	simpld	$⊢ φ \to B \in V$
194		ovex	$⊢ (1 \dots M - 1) \in V$
195		ovex	$⊢ (1 \dots N - 1) \in V$
196	194 195	xpex	$⊢ (1 \dots M - 1) \times (1 \dots N - 1) \in V$
197		elmapg	$⊢ (B \in V \land (1 \dots M - 1) \times (1 \dots N - 1) \in V) \to (S \in (B^{((1 \dots M - 1) \times (1 \dots N - 1))}) \leftrightarrow S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ B)$
198	193 196 197	sylancl	$⊢ φ \to (S \in (B^{((1 \dots M - 1) \times (1 \dots N - 1))}) \leftrightarrow S : (1 \dots M - 1) \times (1 \dots N - 1) ⟶ B)$
199	189 198	mpbird	$⊢ φ \to S \in (B^{((1 \dots M - 1) \times (1 \dots N - 1))})$

Metamath Proof Explorer

Theorem smatrcl

Proof