Metamath Proof Explorer

Theorem smatrcl

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

Ref Expression
Hypotheses smat.s 
|- S = ( K ( subMat1 ` A ) L )
smat.m 
|- ( ph -> M e. NN )
smat.n 
|- ( ph -> N e. NN )
smat.k 
|- ( ph -> K e. ( 1 ... M ) )
smat.l 
|- ( ph -> L e. ( 1 ... N ) )
smat.a 
|- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
Assertion smatrcl 
|- ( ph -> S e. ( B ^m ( ( 1 ... ( M - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )

Proof

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