smatrcl

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

	Ref	Expression
Hypotheses	smat.s	⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
	smat.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	smat.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	smat.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑀 ) )
	smat.l	⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
	smat.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑_m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
Assertion	smatrcl	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐵 ↑_m ( ( 1 ... ( 𝑀 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem smatrcl

Proof